Stockholm Central Station

Formal Verification to Improve Safety Assessment Process

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.

Infrastructure Manager

Trafikverket/Swedish Rail

Signaling system

Relay-based interlocking system for mainline railway network, just north of Stockholm Central.

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.