Formal Proof Process for the Safety of a Signaling System

The process of formally proving safety for a signaling control system consists of two stages:

1. Phase 1: Through an in-depth analysis of the system requirements, the team constructs a mathematical proof demonstrating how the system’s design principles systematically mitigate all identified risks. Each hypothesis necessary for this proof is clearly articulated and documented.
2. Phase 2: The team then verifies that each hypothesis of the proof has been thoroughly addressed by the various subsystem suppliers and operational procedures. This rigorous step ensures that there are no safety issues in the subsystem specifications, guaranteeing that the final system addresses each safety requirement.

The use of mathematics in this approach significantly enhances confidence in the system’s safety. The hypotheses, which characterize the expected properties of each subsystem, are precisely formalized. This formalization includes rigorous technical arguments that eliminate identified risks such as collisions, derailments, or overspeeding. These properties serve as stringent safety requirements for subsystem development and operational constraints.

Throughout this process, close collaboration among the formal team, project management, and engineering teams is essential. Regular technical exchanges foster a comprehensive understanding of the system, and dedicated workshops are organized to discuss reasoning and hypotheses. This collaborative effort ensures the adequacy and accuracy of the chosen hypotheses.

In summary, formal verification of safety reasoning greatly enhances confidence in the system’s safety. The proof relies on a minimal set of hypotheses that are systematically verified to mathematically eliminate any risk of accidents. This activity, conducted in collaboration with stakeholders, transparently articulates and substantiates the safety reasoning behind the system engineering decisions.

This process, invented by CLEARSY, is used for signalling systems managed by RATP, SNCF and MTA.