In this project Prover Technology collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized interlocking by Thales for several metro lines, and wanted to establish the safety of the interlocking software using formal proof, in a process compliant with CENELEC EN 50128. The solution established was based on:
- Generic, formal safety requirements, based on non-collision and non-derailment properties
- An environment model for train behavior, taken into account in the safety verification
- A sign-off safety verification tool based on Prover Certifier, providing independent formal proof that the interlocking software, including its compiled, binary image, meets the safety requirements.
The solution was first evaluated in parallel with a traditional testing effort within the PMI line 3bis project in 2009. Since then, the solution has entered production use for interlocking systems on e.g. Line 12 South (2010), Line 8 (2011), Line 12 North (2012) and line 1 (2013).