Dec 27, 2019
5 min read
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.
