Purpose
Perform formal safety verification to ensure interlocking software supplied by ABB meet the safety requirements of Bane NOR.
Client
Bane NOR (Norwegian National Rail)
Signaling system
Computerized interlocking system Merkur, by ABB
Formal Safety Verification of Interlocking Software
In projects for Bane NOR’s Nordlandsbanen line, the Ganddal freight terminal and the double track Sandnes-Stavanger, Prover provided turnkey services for safety verification of interlocking software. The interlocking systems were supplied by ABB, and Prover performed projects on behalf of both Bane NOR and its supplier ABB. Prover played a central role in development of the generic safety requirement specification for Norwegian interlocking systems. This specification was maintained in cooperation with Bane NOR and ABB, and was used in a number of projects that applied a two-step process for safety verification of interlocking software using Prover iLock Verifier:
- The interlocking design is formally verified to satisfy the safety requirements.
- The interlocking software is formally verified to ensure that it implements the interlocking design.
By using this process, errors found by formal verification could be removed earlier in the process, saving development resources and improving quality. When all errors had been corrected, formal verification techniques were applied again to ensure the correctness of the final interlocking software for revenue service.
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
Perform formal safety verification to ensure interlocking software supplied by ABB meet the safety requirements of Bane NOR.
Client
Bane NOR (Norwegian National Rail)
Signaling system
Computerized interlocking system Merkur, by ABB
Formal Safety Verification of Interlocking Software
In projects for Bane NOR’s Nordlandsbanen line, the Ganddal freight terminal and the double track Sandnes-Stavanger, Prover provided turnkey services for safety verification of interlocking software. The interlocking systems were supplied by ABB, and Prover performed projects on behalf of both Bane NOR and its supplier ABB. Prover played a central role in development of the generic safety requirement specification for Norwegian interlocking systems. This specification was maintained in cooperation with Bane NOR and ABB, and was used in a number of projects that applied a two-step process for safety verification of interlocking software using Prover iLock Verifier:
- The interlocking design is formally verified to satisfy the safety requirements.
- The interlocking software is formally verified to ensure that it implements the interlocking design.
By using this process, errors found by formal verification could be removed earlier in the process, saving development resources and improving quality. When all errors had been corrected, formal verification techniques were applied again to ensure the correctness of the final interlocking software for revenue service.
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