ClearSy Systems Engineering
Formal method is highly advised by the European CENELEC standards for development of safety critical train control. The major industrials use it for their CBTC and NYCT ( New York metro) is asking their supplier for formal method based demonstration that their CBTC prevents trains from colliding.
Formal data validation is a technique used to automate verification of static data. Very often it is used to check safety parameters of train control and track topology settings. Formal data validation is also widely used by the major railway industrials (Siemens Mobility, RATP, Alstom).
Formal methods are now industry ready, able to scale up to real size railway projects and to provide a real support for successfully completing safety demonstrations.
In this white paper, ClearSy show that several formal methods (B, Event-B, formal data validation) directly contribute to safety critical software development, system-level specification analysis and constant parameters validation, with the help of mathematical proof.
