How to streamline the approval of EULYNX interlockings with Formal Methods

Prover contributing in ForTeS project in Germany for DZSF with DLR

The EULYNX consortium and the Europe’s Rail System Pillar are publishing the specification of the latest generation of interlockings called “digital interlockings”. This is a precise description of interfaces of the interlocking core with its adjacent systems and of the behavior of several adjacent systems, for example, of the point controller. An important goal is to empower infrastructure managers through the standardized modularization of the interlockings to buy subsystems from different suppliers.

EULYNX is a European initiative that standardizes railway signaling interfaces. It enables interoperability between systems, reduces vendor lock-in, and supports modular, digital, and cost-efficient signaling solutions.

Objectives and goals of the project

While many suppliers develop and offer corresponding products, it remains difficult for infrastructure managers to use subsystems of different suppliers as part of the same interlocking. After all, the interoperability of the subsystems and the safe function of the interlocking composed thereof need to be proven – a task for which the supplier of the complete interlocking used to be responsible in the past. Proof and approval of combinations of subsystems from arbitrary suppliers poses a new challenge.

The ForTeS project aims to demonstrate an efficient and reliable approval process for modular systems. This involves two main steps:

1. The first step is about proving that the specification implies the necessary (interoperability, safety) properties. There, the project relies on the extremely rigorous method of formal verification.
2. The second step is about proving conformity of a system implementation to the specification. There, the project relies on highly automated tests as an efficient and broadly applicable method; the certification test cases published by the EULYNX consortium serve as a basis.

Together, these steps will be demonstrated through a simulated approval of a point controller. The resulting assessment report, alongside the formal proof and test suite, will be a key project outcome, helping to accelerate the safe and cost-effective rollout of digital interlockings.

Prover’s contributions

With decades of experience, Prover’s contribution focuses on applying formal methods in railway signaling to ensure compliance with regulatory requirements. Prover will leverage its extensive industry expertise to identify potential applications of formal methods, align them with European railway standards, and reinforce their impact on approval processes. Prover will also evaluate the feasibility and objectives of using formal methods in EULYNX systems, comparing alternative scenarios if applicable.

By contributing to the development of robust and standardized approval methods using Formal Methods, Prover supports the wider adoption of digital interlockings and supports the shift toward more modular, vendor-independent railway systems. This work is closely aligned with our Open Signaling initiative, which promotes openness, transparency, and efficiency in railway signaling to drive innovation and reduce lifecycle costs.

Timeline and project contractors

Project start: May 2025
Duration: 24 months
Main contractor: Prover Technology AB
Subcontractors: Deutsches Zentrum für Luft- und Raumfahrt e.V. (DLR) and ESE Engineering und Software-Entwicklung GmbH

Read the original press release from DZSF (in German):

https://www.dzsf.bund.de/SharedDocs/Standardartikel/DZSF/Projekte/Projekt_205_DSTW-Zulassungsprozesse.html