Purpose
Perform formal safety verification to identify and eliminate errors, to improve the safety assessment process compared to only using traditional, manual review. In particular to find single hardware faults that can cause safety issues.
Client
Trafikverket (The Swedish Transport Administration)
Signaling system
Relay-based interlocking system for mainline railway network, just north of Stockholm Central.
Formal Verification to Improve Safety Assessment Process
Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Trafikverket requires that the changes made to these interlocking systems are verified using formal verification (“maskingranskning”), as these are among the most complex interlocking systems installed in Sweden, and too complex to be verified using traditional methods. Several major changes are made to these systems, to increase traffic capacity through downtown Stockholm.
In this project during 2014-15, consultancy ÅF updated the interlocking system at Karlberg, which connects to the a new 6 km long tunnel with platforms under Stockholm central station as well as to the old part of Stockholm central station. The project verified the safety of the interlocking, including both changed and unchanged parts. It was also ensured that certain design patterns were followed.
The formal verification of this relay-based interlocking type is based on:
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...
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
Perform formal safety verification to identify and eliminate errors, to improve the safety assessment process compared to only using traditional, manual review. In particular to find single hardware faults that can cause safety issues.
Client
Trafikverket (The Swedish Transport Administration)
Signaling system
Relay-based interlocking system for mainline railway network, just north of Stockholm Central.
Formal Verification to Improve Safety Assessment Process
Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Trafikverket requires that the changes made to these interlocking systems are verified using formal verification (“maskingranskning”), as these are among the most complex interlocking systems installed in Sweden, and too complex to be verified using traditional methods. Several major changes are made to these systems, to increase traffic capacity through downtown Stockholm.
In this project during 2014-15, consultancy ÅF updated the interlocking system at Karlberg, which connects to the a new 6 km long tunnel with platforms under Stockholm central station as well as to the old part of Stockholm central station. The project verified the safety of the interlocking, including both changed and unchanged parts. It was also ensured that certain design patterns were followed.
The formal verification of this relay-based interlocking type is based on:
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...
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