Rodin tool
{{Multiple issues|
The Rodin tool is a tool for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method and is intended to be used with an incremental style of modelling. The idea of incremental modelling has been taken from programming: modern programming languages come with integrated development environment 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[according to whom?] 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 of demanding the opposite. The Event-B wiki is a useful user and developer resource[according to whom?].
Rodin (Rigorous Open Development Environment for Complex Systems) is an extension of Eclipse IDE (Java based). Rodin Eclipse Builder coordinates:
- Well-formedness + type checker
- Proof obligation generator
- Proof manager
- 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[citation needed] 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
References
- Jean-Raymond Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996, (ISBN:0-521-49619-5).
- Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, and Laurent Voisin. An open extensible tool environment for Event-B. In Z. Liu and J. He, editors, ICFEM 2006, volume 4260, pages 588–605. Springer, 2006.
- RODIN. Deliverable D18: Intermediate report on case study developments.
- Michael Butler and Stefan Hallerstede :The Rodin Formal Modelling Tool,EU research project IST 511599 RODIN
 |  |
