As railway infrastructure ages across Europe, operators face a critical inflection point. Relay-based signaling systems, some nearly a century old, continue to direct train movements faithfully across thousands of kilometers of track. Yet beneath this reliability lies a growing challenge: the expertise to maintain these systems and access to spare parts needed to repair them.

This guide offers a practical roadmap for infrastructure managers to navigate the increasingly urgent transition from legacy signaling systems to modern, open solutions based on commercial off-the-shelf (COTS) hardware. You’ll discover how digital twins, formal methods, and structured migration processes can transform this complex challenge into a strategic opportunity that will enhance safety, reduce long-term costs, and the possibility to break free from vendor lock-in without disrupting your operations.

Whether you’re planning a complete system overhaul or taking incremental steps toward modernization, this guide provides the framework and real-world examples needed to secure your railway’s signaling future in an increasingly digital world.

The need for migrating old signaling systems to modern open solutions based on COTS hardware

Relay-based signaling systems have long been the backbone of railway operations. While experts predict these systems will remain in use far beyond 2030, a growing challenge is emerging: relay expertise and spare parts are rapidly disappearing. Many organizations face a critical knowledge gap, with limited documentation and resources. This is one of the main drivers for the need to start planning a migration project. Without action, the risk of losing essential know-how increases over time.

Background and motivation

In the realm of railway software development, adhering to industrial standards is not just a matter of compliance; it’s a cornerstone of ensuring safe, reliable, and efficient railway systems. The latest milestone along this journey is the introduction of the CENELEC standard EN 50716:2023. This new standard represents a significant leap forward compared to its predecessors, EN 50128:2011 (and its amendments A1 and A2) and EN 50657:2017 while maintaining a smooth transition from its predecessors and a closer alignment with the railway RAMS standards (EN 50126 and EN 50129).
This development holds significant importance for us at Prover, given our intimate connections with these standards, wherein we provide EN 50128-compliant software tools and applications. Thus, we have thoroughly studied EN 50716 and are excited to share our findings and thoughts here in this blog post. Join us as we delve into the nuances of this latest standard, exploring both its implications and potential impacts.

Formal methods become HR for all SILs

The “Highly Recommended (HR)” endorsement of the Formal Methods technique has now extended to also include lower SILs (e.g., SIL 1 and SIL2 which used to be only R).

As a longstanding believer and practitioner of Formal Methods, we are delighted to see the further endorsement of EN 50716 for the technology. Thanks to advancements in technology and much-improved usability over the years, which Prover has contributed to, Formal Methods have become the efficient and cost-effective approach for rail systems they are today.

Tool diversity

Originating from Clause 6.7.4.4 c of EN 50128, the “tool diversity” concept was introduced in Amendment A2:2020 of EN 50128 and then included in EN 50716. The concept of tool diversity concerns classes T2 and T3 of tools. Model checkers (such as Prover PSL) and testing-related software utilities fall into the class of T2 tools, which is specifically designed for verifying code or data. In contrast, T3 tools are involved in the creation or transformation of code, commonly represented by code compilers and generators. Essentially, tool diversity allows T3 tools to delegate (some) trust to T2 tools, see a quote from the clause:

“Use one tool to perform the function and subject its output to verification of results by an independent tool… for example a rule-checking tool to confirm that the output conforms to all relevant rules.”

This represents a significant evolution from our perspective, as it aligns seamlessly with the principles of our Signaling Design Automation (SDA) solution Prover Trident, which was established many years ago. The independent T2 and T3 tools of the Prover Trident tool suite are Prover Certifier and Prover iLock, respectively. The application software code generated from Prover iLock (based on some GA) can be checked independently by Prover Certifier for conformance to formalized safety requirements (ref. “conforms to all relevant rules”). Therefore, the evidence for Prover iLock working correctly and safely can be based on the use of Prover Certifier, which is highly trusted and certified by TÜV NORD as a CENELEC EN50128-compliant T2 tool for SIL 4 applications.

Annex C

This annex in EN 50128 has been replaced with Annex C “Guidance on software development” in the new standard EN 50716, which now consists of the following three very interesting sections:

• “C.1 Lifecycle model examples”,
• “C.2 Modelling”, and
• “C.3 Artificial Intelligence and Machine Learning”.

Lifecycle models

Section C.1 provides guidance and examples regarding two lifecycle models, i.e., linear lifecycle models (such as the waterfall and v model) and iterative lifecycle models. Linear lifecycle models offer a structured and predictable approach to software development, widely considered the conventional choice. The iterative lifecycle models, on the other hand, prioritize flexibility and responsiveness (to changes), albeit requiring more frequent communication and coordination among team members.

There has been a growing interest in applying iterative models (or agile methodologies) in safety-critical systems including rail systems. We find it interesting that iterative lifecycle models are explicitly accepted by the standard. However, adopting these iterative lifecycle models requires careful consideration to balance flexibility and safety assurance, ensuring that safety and regulatory requirements are adequately addressed. Achieving such a balance can be facilitated by leveraging a model-based approach, adaptability (e.g., utilizing tool diversity as described above), and rigorous methods such as Formal Verification. The automation embedded in formal verification processes enables the assurance of safety with reduced verification times and great certainty. Prover’s SDA approach fits this profile perfectly.

Modeling

In Section C.2, the advantages of modeling approaches are explored, and guidance is provided regarding their application in the context of the standard.

At Prover, we are also excited by this new inclusion in the standard, as modeling (using our formal languages such as PiSPEC, LCF and HLL) serves as one of the cornerstone techniques in the Prover Trident solution and the Digital Twin approach. As highlighted in the excerpt from the standard below, the modeling approach brings even greater benefits when combined with Formal Verification (using formal proofs):

“Models can also reduce the need for certain activities, particularly when using formal proofs.”

AI/ML

Artificial Intelligence (AI), in particular Machine Learning (ML) as the most relevant among the AI areas, is discussed in Section C.3, with respect to the difficult challenges to be addressed in the context of applications in the scope of EN 50716. Because of the challenges (e.g., the V&V of ML components), the ML techniques have not yet become viable techniques for rigorous software development within the standard.

While we agree that it is natural to have such concerns about ML given its inherent characteristics (such as statistical modeling and interpretability), from a different perspective, we at Prover have started to explore how ML techniques can accelerate the adoption of Formal Methods. For more details, see our blog post on AI.

Improvements in management and organization

Following a significant refinement for Clause 5, the requirements on software management and organization have become more concise, succinct, and in some cases relaxed, thereby facilitating users to navigate standards with greater ease and flexibility.

One example of removing/relaxing unrealistic restrictions is the fact that changing the roles of Verifier and Validator is no longer prohibited (but is still discouraged) as outlined in Subclause 5.1.2.10 f of EN 50716, compared to Clause 5.1.2.4 of EN 50128.

The role of Integrator in EN 50128 is removed from EN 50716 and the responsibilities of the role fall under the roles of Implementer and Tester. Instead of the Integrator, the Implementer is supposed to manage the integration process, whereas the Tester is supposed to take responsibility for writing relevant specifications such as the Software Integration Test Specifications and the Software/Hardware Integration Test Specification.

The “Safety Authority” body is no longer relevant in EN 50716. For example, the Assessor has the flexibility to belong to any stakeholder organization without requiring the approval of the “Safety Authority”, as outlined in Subclause 5.1.2.5.

Miscellaneous changes

There are also some changes of various kinds we find interesting and worth highlighting here.

1. EN 50716 switched to “Basic Integrity” defined in EN 50126 and stopped using “SIL 0”, which probably corresponds to one change described in the foreword: “Better alignment with EN 50126-1:2017 and EN 50126-2:2017, including definitions, has been made;”
2. Some justifications and documents are no longer required for the T2 tools used for Basic Integrity. See e.g., Subclauses 6.7.4.2 and 6.7.4.3.
3. Programming languages can also refer to diagrammatical or modeling languages rather than just textual programming languages (such as C, C++, Java, etc.). Additionally, Clause 7.3 (Architecture and Design) introduces criteria for choosing suitable programming languages, which in part replace the requirements related to the fitness for purpose of programming languages (Subclause 6.7.4.7 of EN 50128).
4. In EN 50716, the term “application algorithms” has been removed from the title of Clause 8. This change may clarify that this clause primarily addresses the requirements for application data rather than generic or application software. The application data primarily consists of parameterization information for specific installations and the application software defines the intended behavior (or logic) of specific applications. Prover iLock is a complete development process for signaling systems, particularly application data and software. Hence it is part of our continuous endeavor to maintain its compliance with Clause 8 of EN 50716.

Conclusion

In summary, here at Prover we are leading the way when it comes to embracing the latest advancements within the standard, while continually enhancing our solutions and products to closely align with the requirements of EN 50716. Our dedication ensures that our customers and partners are fully equipped to meet these requirements and thrive in their endeavors.

When developing safety critical rail control software, achieving compliance with safety standards such as CENELEC EN50128 is a significant part of the project. Traditionally, this involves a number of manual steps such as reviewing verification documents, making test plans and reports and, of course, testing itself.

These activities are typically carried out at a later stage of the project, where delays can significantly impact the overall schedule and any issues discovered are costly to address. Furthermore, the highly experienced staff who have the qualifications needed to perform these tasks are often a bottleneck resource.

The solution is to consider safety, and how it is demonstrated, from the start of the project, and to use more automation throughout the verification process. Much of the work of achieving compliance with safety standards can be replaced with Formal Verification. A technique based on mathematical proofs that gives 100% coverage. Since Formal Verification gives full coverage and is fully automated, not only will it increase safety confidence but it will also help reduce the overall cost for safety assessment.

What you will learn in this guide

In this guide, you will learn how to use Formal Verification to meet prevailing safety requirements with full confidence. All while reducing effort, increasing quality, and reducing the risk for project delays in the process.

On the following pages, we will summarize the safety requirements for rail control software set out by the prevailing CENELEC EN 50128 standard, discuss the advantages of using Formal Verification versus traditional system testing methods, and take a closer look at how Formal Verification impacts the verification and validation process and safety approval in rail control projects. Finally, we will explore how Formal Verification is used in practice and offer some recommendations for the implementation process.

In the endeavor to develop rail control software that meets demands for efficient rail transportation— both now and in the future— many of today’s infrastructure managers find themselves impeded by a number of frustrating roadblocks. These include long and unpredictable schedules, a general lack of control over systems, and dominant industry issues such as the current oligopoly of system suppliers.

Recognize these challenges?

As overwhelming as they may be, there is a solution that you as an infrastructure manager can use to overcome them and finally take control over your rail control software development projects. That solution is Signaling Design Automation (SDA) and Digital Twins, and they make it easier to procure, develop and maintain your system software while remaining adaptable to future possibilities.

What to expect from this guide

In this guide, we will run through the basics of how you, as an infrastructure manager, can use SDA and Digital Twins to develop rail control software. You will learn about the advantages of using these tools and how to use them in practice to gain the benefits in your software project. Finally, we will put all of our learnings into perspective with a real-life case study example, and then provide you with some recommendations you can move forward with. Let’s begin!

Advancing the digital transformation is the key to meeting demands for efficient rail transportation, and one important enabler of this is the uptake of new fundamental technologies such as digital twins. In this guide, we focus on how the specification phase of rail control projects can be improved by using formal methods and digital twins. Getting the specifications right from the start, already at the tendering phase, will help you avoid costly specification missteps and, ultimately, carry out a more successful rail control project.

What’s a digital twin and how does it benefit the rail sector?

A digital twin is essentially a virtual, interactive replica of a real physical system, asset or process, including its real-time characteristics and behaviors. Applied to the railway sector, a digital twin encompasses the entire infrastructure – from stations, rolling stock, and signals, to the coordinating IT systems.

Infrastructure managers as well as remote repair crews and station staff stand to benefit from having a digital twin of a railway. With access to a real-time 3D representation of the entire railway infrastructure, maintenance and repairs can be performed faster, and more proactive decisions can be made to prevent safety hazards and costly mistakes, while improving overall efficiency.

But the digital twin is also immensely beneficial when put to use early on – before a railway’s system has even been specified – to ensure the right system is built in the first place.

Using digital twins to develop better rail control systems

Creating a digital twin at the start of a rail control project, before tendering begins, enables infrastructure managers to formulate and evaluate more precise system requirements and, ultimately, procure better systems at a more reasonable price.

At Prover we recommend developing a digital twin by using a process based on formal methods and design automation. This approach minimizes the effort required for development, and provides efficient tools for the simulation, validation and verification of requirement specifications.

Suppliers can use the digital twin as input for the detailed design, using automation tools for code generation, testing, and verification, and further shortening project schedules and reducing costs. The digital twin can then be used throughout the lifecycle of the rail control system, reducing costs related to upgrades and adding new features during the maintenance phase.

What to expect from this guide

In this guide, we will run through the basics of how you, as an infrastructure manager or system buyer, can use formal methods and digital twins to simplify the requirement specification phase and generate the high-quality specifications you need to accomplish your system goals and get your rail control project off to a better start. Finally, we will put all our learnings in perspective with a real-life example. Let’s begin!

If you want to enable safe and reliable rail transportation while making the best use of available infrastructure, implementing efficient rail control and signaling solutions is an essential piece of the puzzle.

The development of these software-based systems is critical in rail transport projects. Delays in delivery, acceptance and safety approvals add up to a highly negative impact on costs and schedules.

There is an obvious need to simplify the rail control solution development process and implement solutions that supply the industry with the tools and processes needed to meet the requirements and expectations of end customers.

How do you do that?

At Prover, we’ve found the formula for a successful rail control project to be threefold: focus on the requirement specifications, use automation to develop the systems, and apply formal and automated methods to prove that requirements and safety are fulfilled.

Not only does this formula generate high-quality software and guaranteed safety, but it can cut both your project time and costs by 50%. Together with more standardization, this paves the way for increased competition and reduced life cycle costs. And, ultimately, a better customer experience with increased traffic capacity and fewer delays.

In this guide, we will walk you through how to use this formula, which is called Signaling Design Automation, to overcome the most common barriers in rail control projects and work smarter to get on the proven track to success.

A typical passenger train weighs between 1500 and 6000 tons and its freight train counterpart weighs more, between 3000 and 18000 tons. Trains are massive. The risks involved in such a mass travelling at high speeds make the safety aspects of the railway industry unique.

Although the industry can pride itself with unusually high standards, each accident has the potential to develop into a major disaster. These risks demand verification techniques that go beyond the limits of testing. This is where the strengths of Formal Verification come into effect.

Download the white paper to see what motivates our conviction.

Guaranteeing safety has been the main objective of rail control, or signaling, systems since the first mechanical interlockings were introduced in Britain in the mid-nineteenth century. As we all know, the complexity of these systems has grown steadily since then, via the relay-based interlockings that were dominant during most of the twentieth century, to the software-based, fully automated rail control solutions of today, often responsible also for the driverless operation of the trains.

The increased complexity and responsibilities of these systems means that it is even more important to ensure that the systems themselves are safe, and a significant part of the software development efforts, and project costs, goes into this safety assurance work. We will here try to give a brief overview of different methodologies and techniques used for this, and also introduce the use of formal verification, an automated verification technique based on mathematics, in this context.

Stockholm Metro has a diverse and complex network with light rail, suburban rail and subway systems. Its signaling systems are a mix of computerized and relay-based interlockings, with modern, centralized traffic management systems.

Maintaining and upgrading these systems to the standards of a modern mass transit facing ever increasing passenger numbers is challenging, from a cost and resource perspective as well as from a safety perspective. In order to address this, Stockholm Metro has deployed modern Signal Design Automation processes covering both safety verification and development of interlocking application software.

In this guide we will take a closer look at two distinct projects of Stockholm Metro; the extension of one of the subway lines using legacy Union Switch & Signal relay-based interlocking and the capacity increase project on a suburban rail line utilizing modern computerized interlockings. The relay-based interlockings are designed using traditional methods but with automatic checks of schematics, and safety is verified with automated formal verification. The computerized interlockings are generated, tested, and verified with a design automation process based on generic and formalized requirement specifications.