• Rodin: The ADVANCE Project is building on the open source Eclipse-based Rodin toolset for Event-BRodin includes a range of automated provers for formal verification of model properties and these are being improved within ADVANCE.
  • ProB: Extensive use is also made of the ProB animator and model checker for Event-B which is integrated into Rodin as a plug-in.

As well as maintaining the core Rodin platform, ADVANCE is developing new tool features as plug-ins to the Rodin platform relevant to engineering of cyberphysical systems.  

Rodin and the other ADVANCE plug-ins are freely available and may be downloaded.

  • ADVANCE Multi-simulation Framework: While mathematical proof is at the core of the Event-B method, simulation plays an important role in ensuring the validity of any formal model. The primary objective of the ADVANCE multi-simulation framework is to address the needs for different design and verification tools, both discrete and continuous, test-based and formal to cooperate within a single development and verification framework.   We aim to support simulations of composition of models and implementations in other languages with Event-B models.  To this end we have decided to adopt the Functional Mock-up Interface (FMI) Standard ( to support integration of simulation tools.
  • Graphical Modelling with UML-BUML-B provides a modelling language that is easier to present system behaviour to working engineers than plain Event-B. In ADVANCE we continue to evolve UML-B to support strong integration with Event-B and with the multi-simulation framework through component diagrams.
  • Graphical Animation with BMotion Studio: BMotion Studio is a visual editor which enables the developer of a formal model to set-up easily a domain specific visualisation. In ADVANCE, BMotion Studio is being extended with a range of customisable graphical idioms to support graphical simulation of cyberphysical systems.