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 project references
In this project, Prover enabled a safe and stepwise migration from legacy relay systems to a modern, PLC-integrated Traffic Management System for the Stockholm Metro.
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
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...
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 project references
In this project, Prover enabled a safe and stepwise migration from legacy relay systems to a modern, PLC-integrated Traffic Management System for the Stockholm Metro.
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
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...
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