Case Studies Trafikverket

Formal Verification of relay-based interlocking systems at Trafikverket

Prover Technology has delivered a variety of software solutions and services to Trafikverket (Swedish National Rail) over the last ten years, including formal safety verification of a number of interlocking systems using Prover iLock (“maskinell säkerhetsgranskning”).

Prover iLock has been used to verify two of Scandinavia’s largest and most complex interlocking systems: Stockholm Central and Karlberg stations. These systems are owned and operated by Swedish National Rail. The stations are implemented with a total of more than ten thousand free-wired vital relays. The relay logic was formally verified to comply with the customer‘s control tables and signaling diagrams, that expresses safety requirements, during both normal and fault mode operation. As part of these projects, Prover Technology also automated client processes by developing custom solutions for automatic database reviews, wiring diagram extraction, and generation of power and terminal post coupling schematics.

In order to automate the verification flow, Prover Technology has developed two translator tools for

  • Automatic extraction of Prover iLock Data from graphical schematic drawings.

  • Automatic conversion of the control tables into Prover iLock safety requirements.

Prover Extractor

The translator tools are capable of checking their output for consistency to ensure that the translations were done correctly and catch "simple" errors like typos in tables and schematics. In addition, fault modes for the relay components were defined in order to enable verification of safety requirements under the assumption that there are hardware faults. Trafikverket typically requires that safety requirements are fulfilled even if a single hardware component fails.

If there are any scenarios in which the properties do not hold, the exhaustive safety verification techniques will detect them and present them for analysis. For the Årstabron system, the verification covered 1685 safety requirements, which were all exhaustively verified by Prover iLock.