ADVANCE Tools
- Rodin: The ADVANCE Project is building on the open source Eclipse-based Rodin toolset for Event-B. Rodin 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 (www.fmi-standard.org) to support integration of simulation tools.
- Graphical Modelling with UML-B: UML-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.