EULYNX: Standard Interfaces for Railway Signaling and the Case for Formal Methods

Railway signaling has long carried a structural problem hiding in plain sight. The interlocking, cornerstone of railway safety, cannot act on its own: it depends on the field elements and their controllers, which move and monitor the trackside (points, signals, train detection, level crossings) and report their state back so the interlocking can reason about it. Nor does it act alone in the other direction: it takes commands from the traffic control system, coordinates with neighboring interlockings across area boundaries, and feeds the radio block centre that issues movement authorities to ETCS trains. Each of those boundaries is an interface across which commands and status flow, and each one divides responsibility for safe behavior. Safety is enforced throughout the system, but with modular architecture the argument for it has to be assembled across those lines. For decades those boundaries have been proprietary, and across most of the installed base they still are. A signaling installation arrived as one supplier-specific package: interlocking, field elements, diagnostics, communications and the links to neighboring areas, each designed to fit the others and nothing else. Once an infrastructure manager committed to one vendor, changing any one part years later, whether a point controller, a level crossing, the neighboring interlocking or the diagnostic system, often meant re-procuring, re-engineering and re-approving a large slice of the system. Innovation slowed, lifecycle costs climbed, and competition narrowed.

EULYNX is the European answer to that problem: a standardized reference architecture, defined by the infrastructure managers themselves, covering the subsystems of a signaling system, the interfaces between them, and the design paradigms they share. It is now moving from specification into live deployment, and as it does, a gap opens that goes to the heart of what Prover does. The interfaces are standardized. The evidence that they hold is not.

Adoption brings three problems with it: interoperability nobody has proven, specification ambiguity that surfaces during integration, and approval cycles that still run on manual review and hand-written tests. Adoption has standardized the interfaces faster than it has produced evidence, and Prover closes that distance three ways: exhaustive proof of conformance, test suites generated from the formal model, and verified adapters for existing products. Read on for how each of these closes a specific gap that EULYNX adoption is now running into, or come find us at InnoTrans 2026 (Hall 3.2, Stand 210) to talk it through in person.

What EULYNX actually is

EULYNX was launched in 2014 and now counts nineteen infrastructure managers, and they publish the result openly: the specifications are released as Baseline Sets under the European Union Public Licence, and since 2023 they have been issued jointly with Europe’s Rail, whose System Pillar now holds technical authority for the shared documents. Baseline Set 4 was closed to functional changes in June 2025, so what suppliers build against is stable. The development goals are stated plainly in the specifications: subsystems should be interchangeable irrespective of supplier, the diversity of communication technology, energy supply and diagnostics should come down, maintenance should be simpler, and lifecycle cost should fall. All of it has to meet the RAMS (reliability, availability, maintainability, safety) targets of the conventional interlockings it replaces, and RAM, safety and security requirements have to be allocated systematically across the subsystems.

EULYNX is not trying to make every railway in Europe operate identically. National operating rules, interlocking principles and commercial interests differ, and they are not going away. EULYNX absorbs that through variability management: IM-specific requirements, including ones that conflict with each other, are carried as configuration through the whole development process instead of being negotiated away. What EULYNX standardizes first is the boundary between components, the interfaces, so that what crosses them is predictable even when the implementations behind them are not. Detailed implementation prescription, down to software and hardware architecture, is deliberately excluded from the standard, which is what leaves manufacturers free to solve the problem their own way.

The architecture: a railway as replaceable parts

The mechanism is a modular reference architecture. It has three layers: command and control on top, the interlocking logic at the core, and the wayside objects with their controllers at the bottom. Adjacent systems sit outside the EULYNX system at both ends: above the interlocking, from the traffic control system to the radio block centre and the interlockings of neighboring areas; below it, from external level crossing systems to the point machines and balises the element subsystems drive. For each of them EULYNX specifies the interface and the functions it needs, without standardizing the system behind it. Points, signals, train detection and level crossings are subsystems in their own right, each driven by a controller carrying enough intelligence to manage security, support preventive maintenance, and hold a fail-safe reaction even when communication with the interlocking is interrupted. Those connections are the SCI family. The first five stay inside the system boundary, between the interlocking and its own subsystems; the last four cross it, to systems outside this EULYNX System:

• SCI-P: points
• SCI-LS: light signals
• SCI-TDS: train detection systems
• SCI-LC: level crossings
• SCI-IO: generic input/output
• SCI-CC: the traffic control system
• SCI-ILS: an adjacent interlocking
• SCI-RBC: the radio block centre and the ETCS world
• SCI-LX: an external level crossing system

Each interface is specified down to the information objects, message flows and timing that cross it: how a command is issued, what status comes back, how a connection is initialized, version-checked and recovered after error. Underneath those definitions sits a stack. The application layer is the Process Data Interface, whose generic telegrams open and close a connection and carry the technical identifier of sender and receiver. Below it runs the Safe Communication Protocol, implemented with RaSTA, which provides the safety, retransmission and redundancy layer; the endpoints of a connection are RaSTA endpoints. Each field element subsystem holds exactly one process data connection to the interlocking, and on a multi-element controller several of them can be stacked onto a single RaSTA channel, which cuts the heartbeat traffic and the bandwidth each subsystem instance needs.

Why this matters, and why now

For a decision-maker, the value proposition is direct: when interfaces are open and standardized, the infrastructure manager becomes the system integrator, free to mix suppliers across subsystems and across decades, renewing the installation piece by piece instead of in one disruptive wave. The result is competition, faster innovation, less lock-in and a credible path to lower lifecycle cost.

This is no longer theoretical. Baseline Set 4 is closed to functional changes, so the specification suppliers build against today is stable even as the System Pillar keeps developing the target architecture. A growing number of European infrastructure managers are committing to it, through framework tenders, ERTMS rollouts, and the first EULYNX-based digital interlockings entering service. Adoption is accelerating, but the tooling to verify and approve these multi-vendor systems has not kept pace.

The part engineers should pay attention to: model-based specification

EULYNX does not specify its subsystems and interfaces as prose alone. It uses Model-Based Systems Engineering (MBSE) with SysML. Functional requirements are captured first as use-case scenarios in sequence diagrams, then refined into executable state machines, from which a runnable virtual prototype is generated, so engineers can inject stimuli and observe responses before any hardware exists. Specification is strictly black-box: what goes in and what comes out, with nothing said about how the box works inside, which is exactly what an interface standard should pin down.

This loop runs at the front of the CENELEC EN 50126-1 life cycle, in the phases the infrastructure managers own, before anyone designs or builds anything. The intent is to catch errors at the specification stage, when they are cheapest to fix. The models also become the reference from which suppliers’ conformance test cases can be derived.

It is a genuine step forward, and it leaves one thing open. Executing a model shows how the system behaves in the runs you execute, and says nothing about the runs nobody thought to try. That is where the problems of deployment begin.

The three problems EULYNX adoption is now hitting

As EULYNX moves into deployment, three hard problems surface, and none of them has a widely adopted automated answer yet.

1. Unproven interoperability. Responsibility for safe behavior has shifted from a single supplier to the integrator, but there is no automated process for proving that a combination of subsystems from different vendors composes safely. The risk is that unsafe combinations are only discovered late, or not at all.
2. Specification ambiguity. The EULYNX specifications are detailed and their models are executable, but the semantics of those models are not formally defined. Two implementers can read the same state machine and build behavior that differs in the corners. Inconsistencies, ambiguities and missing edge cases tend to surface during integration, where they are expensive to fix and trigger repeated approval cycles. These are exactly the kinds of defects that systematic formal analysis is built to uncover.
3. Approval bottlenecks. Compliance validation still leans heavily on manual review and hand-written testing. Approval cycles run long, and each configuration variant repeats them, which is a real brake on Europe-wide EULYNX rollout.

Where formal methods fit, and where Prover comes in

Simulation has a known limit: running scenarios show a system behaves correctly in the cases you happened to try. It cannot prove a hazardous state is unreachable across every possible sequence of events. Formal verification can: it provides mathematical proof that a safety property holds for the model of the system. That is the difference between “we didn’t find a problem” and “a problem cannot exist.”

This is the gap Prover has spent its history closing, and it bears directly on the problems above. Prover brings three capabilities to it:

1. Compliance evaluation. Prover maintains a precise, executable reference model of the EULYNX specification, expressed in Prover’s HLL and sHLL languages. Prover PSL uses that model to prove exhaustively that a supplier’s software conforms to the standard: that the implementation satisfies the safety, behavioral and protocol properties EULYNX requires. Compliance is established by formal proof rather than manual review, and the evidence is fully traceable and independently reproducible through Prover Certifier, a TÜV NORD-certified CENELEC EN 50128/50716 T2 tool qualified for SIL 4 work.
2. Test-suite generation. Prover derives structured, high-coverage test suites directly from the EULYNX formal model, going beyond the published certification test cases and ready for hardware-in-the-loop testing. This automates what is today painstaking manual test design, compresses approval timelines, and catches interaction edge cases that hand-written tests miss.
3. Compliant adapters. Most of what is running today was never built to EULYNX, and none of it is being replaced wholesale. Prover develops verified adapters that convert existing non-EULYNX modules into EULYNX-compliant subsystems, translating between legacy and standardized interfaces with formal guarantees that the translation preserves the required behavior. This lets suppliers bring proven products into the EULYNX ecosystem without redesigning from scratch, and lowers the adoption barrier for infrastructure managers, part of the broader open signaling initiative toward an open, interoperable signaling stack.

There is a deeper alignment at work here. EULYNX has already done the hard cultural work of moving an industry from prose requirements toward formal, executable artifacts. Formal methods are the natural next layer on that foundation: they consume exactly the kind of rigorous model EULYNX now produces, and return exactly the kind of evidence a safety case needs. The two are consecutive steps in the same argument.

Working with us

Whether you are an infrastructure manager evaluating digital interlockings or needing formal evidence of conformance before procurement, a system integrator proving multi-vendor configurations safe, a supplier bringing an existing product into the EULYNX ecosystem, or a certification or assessment team that needs reproducible evidence rather than test reports alone, the same three capabilities apply to your work.

What we deliver is formal evidence of EULYNX compliance for the interfaces, subsystems and systems you need to evaluate, test or adapt, produced with tools certified for SIL 4 applications and independently reproducible by an assessor.

To discuss how formal methods can support your EULYNX compliance, book a technical review with the Prover team. And if you are going to InnoTrans 2026, come to Stand 210 in Hall 3.2, where we can walk through what a completed conformance proof actually contains.