Purpose
Establish automated sign-off safety verification based on mathematical proof, in a process compliant with CENELEC EN 50128.
Client
Infrastructure Manager RATP (Paris Metro)
Signaling system
Computerized interlocking systems based on the PMI platform by Thales
Automated Sign-off Safety Verification compliant with CENELEC EN 50128
In this project Prover 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:
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).
Related case studies
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...
Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Swedish Rail requires that the safety of changes made to these interlocking systems is verified using...
In this project, Ansaldo STS delivers the wayside systems to Trafikverket’s ERTMS Level 2 project ESTER, including a new computerized interlocking system. Trafikverket requires that their...
How much can you save by implementing Signaling Design Automation?
In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.
Purpose
Establish automated sign-off safety verification based on mathematical proof, in a process compliant with CENELEC EN 50128.
Client
Infrastructure Manager RATP (Paris Metro)
Signaling system
Computerized interlocking systems based on the PMI platform by Thales
Automated Sign-off Safety Verification compliant with CENELEC EN 50128
In this project Prover 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:
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).
Related case studies
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...
Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Swedish Rail requires that the safety of changes made to these interlocking systems is verified using...
In this project, Ansaldo STS delivers the wayside systems to Trafikverket’s ERTMS Level 2 project ESTER, including a new computerized interlocking system. Trafikverket requires that their...
How much can you save by implementing Signaling Design Automation?
In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.
+46 (0)8 617 68 00