Rodin Plug-ins

For developer support, see Rodin Developer Support

Rodin Plug-in Documentation

Text Editor augments the standard structured editor of Rodin with a text editor.
Rodin Editor augments the standard structured editor of Rodin with a structured text based editor.
CamilleX (formerly XEvent-B) with support for text editors and modelling mechanisms such as machine inclusion.
Records provide structured types for Event-B.
UML-B provides a 'UML-like' graphical front end for Event-B.
Parallel Composition using Event-B allows the composition of machines through events for Event-B.
Decomposition Plug-in allows the decomposition of Event-B machines/contexts (shared variables (A-style) and shared events decomposition (B-style))
Refactoring Framework allows the refactoring of elements that are part of file (and also on related files).
Rose (Structured) Editor a model structured editor.
Flows plug-in allows the addition of control flow to a machine.
Modularisation Plug-in provides a mechanism for constructing and proving modular developments.
Mode/FT Views plug-in brings modelling of modal and fault tolerance features.
Team-based development enables Event-B models to be stored in a shared repository (e.g. SVN).
Qualitative Probability provides supports for reasoning about termination with probability 1 (almost-certain termination).

ProB is an animator and model checker for the B-Method,
AnimB is an animator for the Rodin platform,
UML-B - Statemachine Animation provides an animation (using Pro-B) of UML-B State-machines,

BMotion Studio a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization.

Isabelle for Rodin: Prove proof obligations with Isabelle/HOL. Export proof obligations to Isabelle/HOL theories.
Theory Plug-in provides capabilities to extend the Event-B mathematical language and the Rodin proving infrastructure.
Proof Purger offers to delete unused proofs.
Proof Skeleton View displays the skeleton of existing proofs.
SMT Plug-in provides interface for SMT solvers.
Relevance Filter Plug-in Uses heuristics to filter hypotheses shown to the prover

EventB2Java generates JML-specified Java implementations of Event-B models. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
EventB2JML translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
EventB2Dafny translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.
EventB2SQL translates Event-B machines to Java implementations that make the state of a machine persistent by storing it in a database.
EB2ALL (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.
Tasking Event-B supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.
B2C translates Event-B models to C source code, which may then be compiled using external C development tools.
EHDL The plug-in enables VHDL code generation from formal Event-B models automatically.

Group Refinement changes the set of refinement laws for one refinement step to facilitate a case of atomicity refinement.
Model Critic is an extension using the Epsilon scripting language to analyse Event-B models
Feature Composition Plug-in allows the composition of Event-B features (machines|contexts) and helps the user in resolving conflicts before composition.
Feature Modelling Tool (prototype) can be used to build feature models for product lines and configure these to generate product line members.
Pattern allows the reusing of existing models within a development in order to save the modelling and proving effort.
Project Diagram displays the diagram of a Rodin project.
MBT plugin can be used to generate test sequences covering the events of an Event-B model.
Transformation patterns allow writing and running transformation scripts in EOL over Event-B models.