The Rodin tool, for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method

B-Method

The B method is method of software development based on B, a tool-supported formal method based around an abstract machine notation, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation and supports...

 and is intended to be used with an incremental style of modelling

Modeling language

A modeling language is any artificial language that can be used to express information or knowledge or systems in a structure that is defined by a consistent set of rules...

. The idea of incremental modelling has been taken from programming: modern programming languages

High-level programming language

A high-level programming language is a programming language with strong abstraction from the details of the computer. In comparison to low-level programming languages, it may use natural language elements, be easier to use, or be from the specification of the program, making the process of...

 come with integrated development environment

Integrated development environment

An integrated development environment is a software application that provides comprehensive facilities to computer programmers for software development...

 that make it easy to modify and improve programs. The Rodin tool provides such an environment for Event-B.
The two main characteristics of the Rodin tool are its ease of use and its extensibility.
The tool focuses on modelling. It is easy to modify models and try out variations of a model. The tool can also be extended easily. This makes it possible to adapt the tool to specific needs, so the tool can be adapted to fit into existing development processes instead demanding the opposite.

Rodin (Rigorous Open Development Environment for Complex Systems) is

• Extension of Eclipse
  Eclipse (software)
  Eclipse is a multi-language software development environment comprising an integrated development environment and an extensible plug-in system...
  
  IDE (Java based)
• Rodin Eclipse Builder coordinates:
  • Well-formedness + type checker
  • Proof obligation (PO) generator
  • Proof manager (PM)
  • Propagation of changes

Rodin Proof Manager (PM)

• PM constructs proof tree for each PO
• Automatic and interactive modes
• PM manages used hypotheses
• PM calls reasoners to
  • discharge goal, or
  • split goal into subgoals
• Collection of reasoners:
  • simplifier, rule‐based, decision procedures, …
• Basic tactics language to define PM and reasoners

Industrial applications and case studies

The Rodin project included five industrial case studies that served to validate the tool set and
helped with the elaboration of an appropriate methodology for using the tools. The case studies
were led by industrial partners of the Rodin project supported by the other partners. The case
studies were as follows:

• a failure management system for an engine controller
• part of a platform for mobile Internet technology
• engineering of communications protocols
• an air-traffic display system
• an ambient campus application

Some available plug-ins for Rodin

• B4free provers
  • Provider: ClearSy
  • Function: Theorem provers
• UML-B
  • Provider: University of Southampton
  • Function: UML-like graphical front-end for Event-B supporting class diagrams and state charts
• proB
  • Provider: University of D¨usseldorf
  • Function: Animation and Model-checking of Event-B models; Counterexamples for false proof goals, in particular, proof obligations
• Brama
  • Provider: ClearSy
  • Function: Animation of B models. The purpose is twofold:
    • experimentation with a model to observe states and transitions
    • Flash animation of Event-B models