ERTMS L2, Sweden

Formal Specification and Approval of Safety compliant with CENELEC SIL-4

Purpose

Safety assessment of interlocking software, by formal verification of Trafikverket’s safety requirements, and including safety verification report in Safety Case.

Infrastructure Manager

Trafikverket/Swedish Rail

Signaling system

Computerized interlocking M11 for ERTMS Level 2, by Ansaldo STS

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 supplier demonstrates the safety of the interlocking systems using formal verification, based on a set of safety requirements provided by Trafikverket. For the pilot line Haparandabanan in northern Sweden, Ansaldo STS licenses and uses Prover Certifier to perform the formal safety verification, and providing a safety verification report as part of the Safety Case. The technical solution is based on:

Formal specification of the safety requirements (based on Trafikverket’s requirements expressed in natural language) and the configuration of the interlocking under verification
Using a Prover Certifier-based tool chain that incorporates translation of interlocking software design into a formal model and that verifies the safety requirements
Creating a verification report based on the analysis results to form CENELEC SIL 4-compliant safety evidence included in the overall safety case