Event-B and the Rodin Platform

Event-B is a formal method for system-level modelling and analysis. A key feature of Event-B is the use of refinement to represent systems at different abstraction levels, from system-level functional and safety requirements down to detailed component designs. Mechanised proof and model-checking are used to verify consistency and provide traceability between modelling levels.

The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and verification. Rodin is open source and is further extendable with a range of plugins, including graphical UML-based modelling, model-checking, simulation, requirements traceability and code generation.

Technological advantages of intelligent agent technology

• Traceable model-based development and verification, from conception to certification
• Supports DO-254/178C flows for design assurance of airborne electronic hardware and software
  • DO-331 addressing model-based development and verification
  • DO-333 addressing formal methods to complement testing
• Formal proof, model-checking, model-based testing, graphical animation
• Hybrid discrete/continuous multi-simulation supporting the FMI standard
• Combines formal and simulation-based verification with MC/DC coverage closure

Technology roadmap

The development of Rodin was supported by the EU ICT project, ADVANCE: www.advance-ict.eu (2011 – 2014). Originally Rodin development was funded by the EU project Deploy (2008 – 2012) and Rodin (2004 – 2007).

Dec 2013: Adopts the functional mockup interface (FMI) standard for multi-simulation

June 2014: Supports model-based testing and MC/DC coverage

June 2015: Fully integrated proof, model-checking and multi-simulation in a model-based development and test environment