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 reﬁnement to represent systems at diﬀerent abstraction levels and the use of mathematical proof to verify consistency between reﬁnement 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.