Skip to main navigationSkip to main content
The University of Southampton

Event-B and the Rodin Platform

Model-based development and verification for software-intensive systems


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: (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

June 2017: Support for generic reusable validation and verification

Collaboration opportunity

Rodin is already being applied to large-scale industrial developments in the railway, smart grid, defence and automotive domains. We are interested in collaborative R&D projects involving the incorporation of Rodin into industrial design and certification flows. Commercial services are available for Rodin training, plug-in development and consultancy.

If you would like to know more, please contact Michael Butler

Related Staff Member

Privacy Settings