Nowadays, the necessity of formal methods as an essential step in the design process of industrial safety-critical systems is widely recognized.
In its more general definition, the term formal methods encompasses all notations having a precise mathematical semantics, together with their associated analysis and development methods, that allow to describe and reason about the behaviour and functionality of a system in a formal manner, with the aim to produce an implementation of the system that is provably free from defects.
Railway signaling has been traditionally considered as one of the most fruitful areas of intervention for formal methods (Fantechi, Fokkink, & Morzenti, 2011). Already in the early nineties, a series of railway signaling products have benefited from the application of the B formal method in the design process.
The B method (Abrial, 1996) targets software development from specification through refinement, down to implementation and automatic code generation, with formal verification at each refinement step: writing and refining a specification produces a series of proof obligations that need to be discharged by formal proofs. The B method is accompanied by support tools, which include tools for the derivation of proof obligations, theorem provers, and code generation tools.
The B method has been successfully applied to several railway signalingsignaling systems. The SACEM system for the control of a line of Paris RER (DaSilva, Dehbonei, & Mejia, 1993) is the first acclaimed industrial application of B. B has been adopted for many later designs of similar systems by Matra (now absorbed by Siemens). One of the most striking application has been the Paris automatic metro line 14. The paper (Behm, Benoit, Faivre, & Meynadier, 1999) on this application of B reports that several errors were found and corrected during proof activities conducted at the specification and refinement stages. By contrast, no further bugs were detected by the various testing activities that followed the B development.