Purpose
Establish process for safety approval of interlocking software based on formal verification of NYCT’s safety principles, and apply process for multiple vendors as part of independent safety assessment.
Client
New York City Transit (NYCT)
Signaling system
Computerized interlocking systems from various suppliers including
• Westrace Mk II, by Siemens
• MELLOCK, by Mitsubishi
• iVPI, by Alstom
• Microlok II, by Ansaldo STS
Safety Approval of Interlocking Software based on Formal Verification
New York City Transit (NYCT) is modernizing the signaling system in its subway by installing CBTC and replacing relay-based interlockings with computerized, solid state interlockings (SSIs). Computerized SSI software demands new and improved safety verification, and long-term also reduced cost and time for performing safety verification.
For this purpose, NYCT today requires formal verification of SSI software using Prover iLock Verifier. The safety verification is performed as part of the independent safety assessment (ISA), and checks that NYCT’s generic safety principles are met by the SSI software.
[This verification process is applied for multiple SSI vendors.]
Related case studies
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...
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...
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 process for safety approval of interlocking software based on formal verification of NYCT’s safety principles, and apply process for multiple vendors as part of independent safety assessment.
Client
New York City Transit (NYCT)
Signaling system
Computerized interlocking systems from various suppliers including
• Westrace Mk II, by Siemens
• MELLOCK, by Mitsubishi
• iVPI, by Alstom
• Microlok II, by Ansaldo STS
Safety Approval of Interlocking Software based on Formal Verification
New York City Transit (NYCT) is modernizing the signaling system in its subway by installing CBTC and replacing relay-based interlockings with computerized, solid state interlockings (SSIs). Computerized SSI software demands new and improved safety verification, and long-term also reduced cost and time for performing safety verification.
For this purpose, NYCT today requires formal verification of SSI software using Prover iLock Verifier. The safety verification is performed as part of the independent safety assessment (ISA), and checks that NYCT’s generic safety principles are met by the SSI software.
[This verification process is applied for multiple SSI vendors.]
Related case studies
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...
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...
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