Skip to main navigationSkip to main content
The University of Southampton
Aerospace

Event-B and the Rodin Platform

Model-based development and verification for software-intensive systems

2008-2012

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

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 mjb@ecs.soton.ac.uk

Related Staff Member

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.

×