The activity of formal system proof consists in mathematically expressing the global properties by which system safety is guaranteed, and establishing by mathematical proof that these properties are guaranteed by the local properties of the system’s components.
It is then sufficient to establish that the constituents guarantee their detailed local properties to guarantee system safety thanks to the assurance of this mathematical proof.
Safety reasoning and its proof thus guarantee railway systems. In a first, CLEARSY’s Atelier B tool has just been certified T2 according to the Cenelec EN50129 standard to carry out this proof at SIL4 level.
This approach, now equipped with Atelier B T2 EN50129, has been applied for the CBTCs of the New York (MTA) and Paris (RATP) subways, as well as for the renewal of the Marseille-Ventimiglia line (SNCF, ERTMS system).