Axons
Published in

Axons

Using The Event-B Method For Critical Systems

Event-B is a formal method for system-level modeling and analysis. Key features of Event-B are the use of set theory as a modeling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. The main use for using Event-B is to obtain a formal proof for the main safety properties of the system. Several use cases running in production now are the Ariane 5 rocket, part of the NYC subway line, and part of the Paris Métro line.

Kripke structure

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store