Rodin tool

Rodin
Original author(s)	Jean-Raymond Abrial, Michael Butler, et al.
Developer(s)	European Union Projects: RODIN (2004–2007); DEPLOY (2008–2012); ADVANCE (2011–2014);
Initial release	2007
Written in	Java
Platform	Eclipse IDE
Type	Software tool
License	Open source
Website	www.event-b.org

The Rodin tool is a software tool for formal modelling in Event-B.^[1]^[2] It was developed as part of several collaborative European Union projects, including initially the RODIN project (2004–2007).^[3]

Overview

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. Two characteristics of the Rodin tool are its ease of use and its extensibility.^[2]

The tool focuses on modelling. It allows the user to modify models and try out variations of a model. The tool is also extensible. 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. There is an associated Event-B wiki.^[4]

Rodin ("Rigorous Open Development Environment for Complex Systems") is an extension of Eclipse IDE (Java-based). The Rodin Eclipse Builder manages the following:^[5]

Well-formedness and type checker
Proof obligation (PO) generator
Proof manager (PM)
Propagation of changes

Rodin Proof Manager (PM)

PM constructs a 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 toolset and helped with the elaboration of an appropriate methodology for using the tools.^[6] 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^[7]
- Provider: ClearSy
- Function: Theorem provers
UML-B^[8]
- Provider: University of Southampton
- Function: UML-like graphical front-end for Event-B supporting class diagrams and state charts
ProB^[9]^[10]
- Provider: University of Düsseldorf
- Function: Animation and Model-checking of Event-B models; Counterexamples for false proof goals, in particular, proof obligations
Brama^[11]
- 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
Modularisation^[12]
- Provider: Newcastle University
- Function: Structuring Event-B developments into logical units of modelling, called modules; Model composition; Model reuse

References

^ Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. (2010). "Rodin: An open toolset for modelling and reasoning in Event-B". International Journal on Software Tools for Technology Transfer. 12: 447–466. doi:10.1007/s10009-010-0145-y.{{cite journal}}: CS1 maint: multiple names: authors list (link)
^ ^a ^b Butler, Michael, and Stefan Hallerstede (2007). The Rodin formal modelling tool (PDF). FACS 2007 Christmas Workshop: Formal Methods in Industry. pp. 1–5.{{cite conference}}: CS1 maint: multiple names: authors list (link)
^ "RODIN: Rigorous Open Development Environment for Complex Systems". UK: Newcastle University. Retrieved 13 June 2023.
^ "Event-B and Rodin Documentation Wiki". wiki.event-b.org. Retrieved 13 June 2023.
^ Butler, Michael. "RODIN – the next generation refinement tools" (PDF). UK: University of Southampton. Retrieved 13 June 2023.
^ "Project IST-511599 RODIN "Rigorous Open Development Environment for Complex Systems"" (PDF). UK: Newcastle University. Retrieved 13 June 2023.
^ "B4free as a free-fo-all tool". ClearSy. Retrieved 13 June 2023.
^ "UML-B: Dependable Systems Modelling Language". uml-b.org. Retrieved 13 June 2023.
^ "What is ProB?". prob.hhu.de. Germany: University of Düsseldorf. Retrieved 13 June 2023.
^ Leonova, Mariya Aleksandrovna, and Petr Nikolaevich Devyanin (2022). "Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools". Prikladnaya Diskretnaya Matematika. Supplement 15: 90–99. doi:10.17223/2226308X/15/22.{{cite journal}}: CS1 maint: multiple names: authors list (link)
^ "The Brama animator for RODIN". ResearchGate.net. Retrieved 13 June 2023.
^ "Modularisation Plug-in". wiki.event-b.org. Retrieved 13 June 2023.