Case: Developing digital twins for the Stockholm Metro

When the Stockholm Metro set out to upgrade their rail control system, they contacted us at Prover to assist with the transition.

Stockholm Metro’s system consists of a central traffic management system and a relay-based vital and non-vital signaling system distributed over several relay rooms. The plan is to replace the mechanical control panels used by the operators with a modern computerized traffic management system, as well as to replace the non-vital relays with a distributed PLC solution, and, at least for the time being, leave the vital relays intact.

In order to analyze the existing systems and validate this approach, a digital twin of the system was developed using formal methods. These formal methods included formal specifications with an emphasis on the interface, separation of configuration data and generic requirements, automated simulation-based testing, and formal safety verifications.

CLIENT: Stockholm Metro
LOCATION: Stockholm, Sweden
DATE: 2021-2022

Project goals

In this case, the Stockholm metro had three primary goals. The first was to discover any dependencies that would make it difficult to leave the vital relays untouched.The second was to identify any safety critical functions that are dependent on the existing non-vital relay or control panel design, to include such requirements in the specifications for the new systems. For example, physical wiring may prevent certain commands from being received simultaneously, or safety standards and best practices may have changed since the original system was commissioned. And finally, they wished to test out the concept in order to avoid any surprises that could delay the project and make it more expensive.

PROJECT START

At the start of this project, the Stockholm Metro’s architecture consisted of the following components: 

• Physical maneuver panel – Push/pull buttons and switches for controls, lamps for indications 
• Non-vital relays – Interface between panel and interlocking, with additional (non-safety related) logic 

Vital relays – Safety related signaling logic, locking of routes and points, signal aspects

END GOAL

The end goal of the project was a future architecture consisting of: 

• A computerized traffic management system with an operator interface 
• A set of PLCs with the same functionality as the current non-vital relays 
• The vital relays from the original system left intact, interfacing with the PLCs

The solution in 6 steps

1. Created a digital twin of existing system
2. Carried out formal verification of the safety of the current system
3. Automatically generated the PLC application software 
4. Created a digital twin of the future system
5. Replaced the model of the PLC with an actual PLC
6. Replaced the model of the interlocking with the actual relay system

Results

Following this process, the Stockholm Metro was able to successfully validate the modularity of the proposed system and establish that it is feasible to replace the non-vital relays with a PLC system. They were also able to identify a few unexpected details in the existing system. 

Furthermore, the digital twin validation approach simplified the transition to the physical environment relay system–testing with the PLC installed in the field was conducted over the course of a single night. 

In the future, the Stockholm Metro can use the digital twin for preparing tenders, validation and verification, reproducing issues from field error reports/logs, replacing testing in the field, and training and documentation.