Formal Specification for ERTMS L2, Sweden2018-11-01T10:23:12+00:00

Project Description

ERTMS L2, Sweden

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

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