Portfolio arkiv - Prover - Engineering a Safer World https://prover.com/references/ Interlocking Design Automation to meet demand for complex digital train control Tue, 07 Oct 2025 14:48:10 +0000 en-US hourly 1 https://wordpress.org/?v=6.9.4 Formalizing Trafikverket’s signaling rules with proven methodology https://www.prover.com/references/formalizing-trafikverkets-signaling-rules-with-proven-methodology/ Tue, 07 Oct 2025 14:48:10 +0000 https://www.prover.com/?post_type=avada_portfolio&p=22300 The project formalized Trafikverket’s signaling regulations by translating them into machine readable requirements and building internal competence in formal methods, paving the way for safer, more efficient, and fully digitalized railway signaling.

Inlägget Formalizing Trafikverket’s signaling rules with proven methodology dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

To translate Trafikverket regulations/signalling principles into formal requirements and to increase the knowledge and know-how of formal methods at Trafikverket.

Client
Client

Infrastructure Manager: Trafikverket (The Swedish Transport Administration)

Signaling system
Signaling system

  • Conventional (ATC)

  • ERTMS

Building formal competence for safer and smarter railway signaling

What did we do in forms of technical solution?

Short intro of the project
The project focuses on converting Trafikverket’s signaling regulations (TRVINFRA) into formal requirements to enable digitalization and automation within railway signaling. It is a continuation of earlier work where Prover demonstrated how signaling rules could be expressed in formal logic and verified using model-based tools.

What was the purpose?
The aim is twofold:

  1. To translate Trafikverket’s signaling principles into formal requirements, ensuring that the regulatory framework is unambiguous, structured, and ready for use in design and verification workflows.
  2. To build Trafikverket’s internal competence in formal methods, so the organization can manage, maintain, and extend formalized requirements in the future.

How did we resolve the issue?
Prover contributed expertise in formal methods and tool configuration, guiding Trafikverket in structuring and formalizing requirements using the open HLL language. Workshops and training were held to teach formalization techniques, and example requirements were implemented and validated using Prover iLock. A process for managing and maintaining formal requirements was established, including a governance and documentation plan for future use.

What was the result of the project?
The project contributes directly to Trafikverket’s long-term digitalization goals by introducing a methodology that increases safety, reduces ambiguity in signaling regulations, and improves efficiency in design and verification processes. The collaboration between Prover and Trafikverket also establishes a foundation for future projects involving automated signal verification.

  • Created formal requirements in HLL based on TRVINFRA-00301, -00302, and -00303.

  • Developed logical and information models supporting these formal requirements.

  • Configured and demonstrated verification using Prover iLock.

  • Designed training sessions and exercises for Trafikverket specialists, focused on creating, validating, and maintaining formal requirements.

  • Supported integration with Trafikverket’s design platform SIVERt for automatic quality assurance and signal logic verification.

Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Formalizing Trafikverket’s signaling rules with proven methodology dök först upp på Prover - Engineering a Safer World.

]]> Modernizing Stockholm Metro’s TMS with safe, stepwise migration to PLC https://www.prover.com/references/modernizing-stockholm-metros-tms-with-safe-migration/ Fri, 25 Apr 2025 13:43:30 +0000 https://www.prover.com/?post_type=avada_portfolio&p=21721 In this project, Prover enabled a safe and stepwise migration from legacy relay systems to a modern, PLC-integrated Traffic Management System for the Stockholm Metro.

Inlägget Modernizing Stockholm Metro’s TMS with safe, stepwise migration to PLC dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

To replace outdated mechanical traffic control system with a modern computerized Traffic Management System, enabled by safe and efficient migration of non-vital relay logic to PLC interface.

Client
Client

Client: Cactus Rail
Infrastructure Manager: Stockholm Metro (SL)

Signaling system
Signaling system

Relay-based interlocking system with mechanical operator panels. Migrating to PLC-controlled non-vital interface logic integrated with computerized TMS.

Enabling the transition from legacy systems to modern signaling

In 2024, our partner Cactus Rail AB secured a turnkey contract to deliver a new Traffic Management System (TMS) for the Stockholm Metro, covering 64 stations across the Red and Blue lines. To ensure a safe and efficient transition, Cactus chose to collaborate with Prover – experts in railway signaling and formal methods.

The existing traffic control system, built on mechanical operator panels and non-vital relay logic, is being replaced with a modern architecture. This includes a computerized TMS, a programmable logic controller (PLC) managing non-vital logic, and continued reliance on vital relay interlockings for safety-critical operations.

Prover plays a key role in digital twin modeling the overall system, simulating operations, generating verified PLC logic, and enabling digital testing before deployment. This step-by-step migration approach ensures minimal disruption to a network that serves 250 million passengers annually.

The project marks a major leap in the modernization of Stockholm metro, delivering a future-proof solution that enhances efficiency, safety, and maintainability.

  • Replace mechanical panels with PLC interfaces

  • Connect non-vital logic to computerized TMS

  • Simulate and verify logic with digital twin

  • Migrate step by step with minimal disruption

Case study

Succeed with smooth railway migration

Ensure a safe, efficient transition from legacy signaling systems to modern solutions using digital twins.

Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Modernizing Stockholm Metro’s TMS with safe, stepwise migration to PLC dök först upp på Prover - Engineering a Safer World.

]]> Implementing Prover Trident for SL, Stockholm https://www.prover.com/references/implementing-prover-trident-for-sl-stockholm/ Mon, 03 Apr 2023 17:14:16 +0000 https://stage.prover.com/?post_type=avada_portfolio&p=11893 In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.

Inlägget Implementing Prover Trident for SL, Stockholm dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

Reduce time-to-market for development and safety approval of interlocking software. Establish sign-off safety verification in compliance of CENELEC EN 50128:2011 SIL4.

Client
Client

Infrastructure Manager Stockholm Metro (SL)

Signaling system
Signaling system

Interlocking systems for mainline railway Roslagsbanan, based on the Microlok II platform by Ansaldo STS.

Development and safety approval of interlocking software

In signaling design automation projects, we start by developing a digital twin of your existing systems, future systems and conceptual systems.

The digital twin is developed using formal methods that utilize automated simulation and can test and validate every step of your rail control project.

  • Advancing the digital transformation

  • Specification phase of rail control projects

  • Getting the specifications right from the start

  • Carry out a more successful rail control project.

Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Implementing Prover Trident for SL, Stockholm dök först upp på Prover - Engineering a Safer World.

]]> Our formal verification solution for RATP, Paris https://www.prover.com/references/ratp-paris/ Sat, 10 Dec 2016 10:05:13 +0000 https://www.prover.com/?post_type=avada_portfolio&p=612 In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized...

Inlägget Our formal verification solution for RATP, Paris dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

Establish automated sign-off safety verification based on mathematical proof, in a process compliant with CENELEC EN 50128.

Client
Client

Infrastructure Manager RATP (Paris Metro)

Signaling system
Signaling system

Computerized interlocking systems based on the PMI platform by Thales

Automated sign-off safety verification compliant with CENELEC EN 50128

In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized interlocking by Thales for several metro lines, and wanted to establish the safety of the interlocking software using formal proof, in a process compliant with CENELEC EN 50128. The solution established was based on:

  • Generic, formal safety requirements, based on non-collision and non-derailment properties
  • An environment model for train behavior, taken into account in the safety verification
  • A sign-off safety verification tool based on Prover Certifier, providing independent formal proof that the interlocking software, including its compiled, binary image, meets the safety requirements.

The solution was first evaluated in parallel with a traditional testing effort within the PMI line 3bis project in 2009. Since then, the solution has entered production use for interlocking systems on e.g. Line 12 South (2010), Line 8 (2011), Line 12 North (2012) and line 1 (2013).

Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Our formal verification solution for RATP, Paris dök först upp på Prover - Engineering a Safer World.

]]> Implementing the Prover iLock tool-suite for Canadian Pacific https://www.prover.com/references/canadian-pacific/ Fri, 09 Dec 2016 10:11:42 +0000 https://www.prover.com/?post_type=avada_portfolio&p=616 Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...

Inlägget Implementing the Prover iLock tool-suite for Canadian Pacific dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

Improve capacity and consistency in design and test of interlocking software by using tools for generation and checking based on AREMA signaling principles.

Client
Client

Infrastructure Manager Canadian Pacific (CP)

Signaling system
Signaling system

Computerized interlocking systems with coded track circuits:
• ElectroLogIXS, by General Electric
• Microlok II, by Ansaldo STS

Improve capacity and consistency in design & test of interlocking software

Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated generation of test plans for factory and commissioning tests, to increase quality and consistency.

Today, CP has introduced the complete Prover iLock tool-suite for generation and checking of interlocking software, including a standard set of signaling principles. The signaling principles are CP’s variation of AREMA principles, supporting the coded track circuits, different location types and interlocking hardware platforms that CP uses.

This gives CP and its engineering service providers an off-the-shelf solution for generation and checking of interlocking software. The checking includes formal safety verification with Prover iLock Verifier and functional testing using Prover iLock Simulator. Location-specific test plans for factory and commissioning tests are generated using Prover iLock Documenter.

Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Implementing the Prover iLock tool-suite for Canadian Pacific dök först upp på Prover - Engineering a Safer World.

]]> Formal verification for Stockholm Central https://www.prover.com/references/karlberg-stockholm/ Thu, 08 Dec 2016 10:22:51 +0000 https://www.prover.com/?post_type=avada_portfolio&p=621 Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Swedish Rail requires that the safety of changes made to these interlocking systems is verified using...

Inlägget Formal verification for Stockholm Central dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
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.

Client
Client

Trafikverket (The Swedish Transport Administration)

Signaling system
Signaling system

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

Formal Verification to Improve Safety Assessment Process

Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Trafikverket 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.

logo af

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.
Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Formal verification for Stockholm Central dök först upp på Prover - Engineering a Safer World.

]]> Formal specification for ERTMS L2, Sweden https://www.prover.com/references/ertms-l2-sweden/ Wed, 07 Dec 2016 10:31:41 +0000 https://www.prover.com/?post_type=avada_portfolio&p=631 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...

Inlägget Formal specification for ERTMS L2, Sweden dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

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

Client
Client

Trafikverket (The Swedish Transport Administration)

Signaling system
Signaling system

Computerized interlocking M11 for ERTMS Level 2, by Ansaldo STS

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.

Hitachi Rail STS

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
Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Formal specification for ERTMS L2, Sweden dök först upp på Prover - Engineering a Safer World.

]]> Formal Safety Verification for Bane NOR, Norway https://www.prover.com/references/bane-nor/ Tue, 06 Dec 2016 10:40:29 +0000 https://www.prover.com/?post_type=avada_portfolio&p=636 In projects for Jernbaneverket’s Nordlandsbanen line, the Ganddal freight terminal and the double track Sandnes-Stavanger, Prover provided turnkey services for safety...

Inlägget Formal Safety Verification for Bane NOR, Norway dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

Perform formal safety verification to ensure interlocking software supplied by ABB meet the safety requirements of Bane NOR.

Client
Client

Bane NOR (Norwegian National Rail)

Signaling system
Signaling system

Computerized interlocking system Merkur, by ABB

Formal safety verification of interlocking software

In projects for Bane NOR’s Nordlandsbanen line, the Ganddal freight terminal and the double track Sandnes-Stavanger, Prover provided turnkey services for safety verification of interlocking software. The interlocking systems were supplied by ABB, and Prover performed projects on behalf of both Bane NOR and its supplier ABB. Prover played a central role in development of the generic safety requirement specification for Norwegian interlocking systems. This specification was maintained in cooperation with Bane NOR and ABB, and was used in a number of projects that applied a two-step process for safety verification of interlocking software using Prover iLock Verifier:

  • The interlocking design is formally verified to satisfy the safety requirements.
  • The interlocking software is formally verified to ensure that it implements the interlocking design.

By using this process, errors found by formal verification could be removed earlier in the process, saving development resources and improving quality. When all errors had been corrected, formal verification techniques were applied again to ensure the correctness of the final interlocking software for revenue service.

logo abb
Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Formal Safety Verification for Bane NOR, Norway dök först upp på Prover - Engineering a Safer World.

]]> Formal verification for Infrabel, Belgium https://www.prover.com/references/infrabel/ Sun, 04 Dec 2016 11:40:07 +0000 https://www.prover.com/?post_type=avada_portfolio&p=643 In this project, Prover provided tools and services to help Infrabel increase the quality of requirement specifications for tendering of level crossing systems. Infrabel was preparing to replace...

Inlägget Formal verification for Infrabel, Belgium dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

Formalize and validate a specification of level crossing requirements, using a number of different level crossing configurations, and using formal verification of safety

Client
Client

Infrabel, the Belgian railway infrastructure manager

Signaling system
Signaling system

Computerized level crossing controllers

Formalize and validate safety and design specifications

In this project, Prover provided tools and services to help Infrabel increase the quality of requirement specifications for tendering level crossing systems. Infrabel was preparing to replace about 800 relay-based level crossings with computerized controllers. Due to the safety-critical nature and the complexity of the requirement specifications for these systems, Infrabel decided to perform requirement validation to detect and eliminate specification errors and ambiguities. The purpose of this was to supply increased quality in specifications to suppliers, and thereby reducing the risk of delays in the delivery of computerized rail control. Infrabel selected Prover to do the formal validation of requirement specification, with a technical solution based on;

  • Safety requirements formalized in the PiSPEC language
  • Design requirements formalized in the PiSPEC language
  • Prover iLock tool suite for configuration of level crossing applications and safety verification of the applications

In total 54 families of level crossing configurations were specified (27 with barriers and 27 without), made subject to formal verification of some 119 safety requirements. This helped uncover unexpected behaviour in the level crossing requirement specification and enabled correction and update of the requirement specification prior to the tendering process.

Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Formal verification for Infrabel, Belgium dök först upp på Prover - Engineering a Safer World.

]]> Automated simulation and formal verification for Qinghai Tibet, China https://www.prover.com/references/qinghai-tibet-china/ Sat, 03 Dec 2016 11:44:16 +0000 https://www.prover.com/?post_type=avada_portfolio&p=645 As part of a project for the Ministry of Railways of the People’s Republic of China, GE Transportation supplied 20+ interlocking systems for the Qinghai-Tibet railway. Prover joined this project...

Inlägget Automated simulation and formal verification for Qinghai Tibet, China dök först upp på Prover - Engineering a Safer World.

]]>
Purpose
Purpose

Deploy state of the art safety verification, and to reduce recurring engineering costs for projects that deliver many interlocking systems

Client
Client

Ministry of Railways, PR China

Signaling system
Signaling system

VHLC, by General Electric

Automated simulation and formal verification of interlocking software

As part of a project for the Ministry of Railways of the People’s Republic of China, GE Transportation supplied 20+ interlocking systems for the Qinghai-Tibet railway. Prover joined this project to specify the signaling rules governing test and safety principles for these systems, implemented on VHLC hardware controllers. These test and safety principles were used by GE Transportation to perform automated simulation and formal verification of the interlocking software using the Prover iLock Simulator and Prover iLock Verifier.

Following the success of this project, GE Transportation proceeded to incorporate support for Prover iLock in the VHLC programming tool ACE, so that interlocking software developed with Prover iLock could be imported into ACE.

Related project references
View all
View all

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
New York City Transfer
Siemens
Alstom

Inlägget Automated simulation and formal verification for Qinghai Tibet, China dök först upp på Prover - Engineering a Safer World.

]]>