Foreword

The Rodin tool supports the application of the Event-B formal method. It provides core functionality for syntactic analysis and proof-based verification of Event-B models. Rodin also provides extension points for a range of additional plug-ins that enrich the core functionality through support for features such as model checking, model animation, graphical front ends, additional proof capabilities and code generation.While the B Method, developed by Jean-Raymond Abrial in the early 1990s, is focused on supporting formal development of software, Event-B broadens the perspective to cover systems; instead of just modelling software components, Event-B is intended for modelling and reasoning about systems that may consist of physical components, electronics and software. An essential difference between Event-B and the B Method is that Event-B admits a richer notion of refinement in which new observables may be introduced in refinement steps; this means that complex interactions between subcomponents may be abstracted from in early stage modelling and then introduced through refinement in incremental stages.

At around the same time that Jean-Raymond was developing the concepts in Event-B, I was involved in an initiative with the University of Newcastle (Alexander Romanovsky, Cliff Jones), bo Akademi (Kaisa Sere, Elena Troubitsyna) and Jean-Raymond to put together an EU proposal on formal methods for dependable systems. That became the RODIN project (2004 to 2007) and a key part of the project was the development of an open source extensible toolset to support refinement-based formal development. Many of Jean-Raymond’s ideas on Event-B were worked into the requirements for the tool and the development of the core tool platform was led by Jean-Raymond and Laurent Voisin (both then at ETH Zurich). Thorough analysis was undertaken to determine that Eclipse was the right platform on which to build an open toolset. The ease with which the core may be extended with plug-ins from a range of teams to provide seamless functionality indicates this was a good decision. The tools developed in the RODIN project took on the name of the project and, since it had a certain cachet, it was decided to retain the Rodin name for the tool after the project ended.

The RODIN Project was followed by the DEPLOY Project which addressed further development of the Rodin core and associated plug-ins in parallel with industrial-scale deployment of the Rodin tools. Exposing the tools to serious industrial users in DEPLOY drove the developers to implement significant improvements in performance, usability and stability of Rodin and key plug-ins such as ProB, the Theory plug-in, Camille and UML-B. Of course, as well as demanding improvements to the tool, the industrial users demanded documentation on the tool, which led to this handbook. Michael Jastram and the team at Düsseldorf have done an excellent job in pulling together, extending and improving various sources of documentation on the Rodin tool. Like the Rodin tools, it will serve as a valuable resource that will continue to evolve beyond the DEPLOY project.