Stockholm Central Station
Formal Verification to Improve Safety Assessment Process
Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Swedish Rail 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:
- Generic safety requirements plus specific requirements in control tables and signaling charts.
- Prover Extractor for extracting a formal verification model from relay schematics, and Prover iLock Verifier for safety verification.
- The Cst toolbox including templates, a relay database, and a library of schematic cells.