Prover at ISoLA 2026: three papers on formal methods for railway signaling

We were pleased to be part of ISoLA 2026 conference (International Symposium on Leveraging Applications of Formal Methods) on October 24-28 in Kos, Greece, with three papers on formal methods for railway signaling.

Two of them come out of the ForTeS project and cover our work on formal verification and testing of EULYNX specifications: how we build formal models from the SysML models, what we prove on them with Prover PSL™, and how the same models serve to execute and generate conformance tests. The third extends the picture to ETCS (European Train Control System) trackside systems and their architectural variants, validated in one ontology-driven framework.

• “Making SysML State Machines Correct: A Prover Formal Verification Approach” – Benjamin Blanc, Abderrahmane Feliachi, Rong Gu
• “Formal Verification and Testing of EULYNX Specifications” – Benjamin Blanc, Abderrahmane Feliachi, Rong Gu
• “Architectural Variants of ETCS-Based Trackside Systems in a Unified Ontology-Driven Validation Framework” – Arne Borälv, Daniel Schwencke (DLR)

Making SysML State Machines Correct: A Prover Formal Verification Approach

EULYNX standardizes the interfaces between interlockings, field elements and adjacent systems, and its specifications are written as SysML state machines. When subsystems come from different suppliers, interoperability and safety have to be argued on the specification itself. That only works if the state machines in it are correct.

In the ScaIVeri track, we presented how we translate each SysML state machine into a formal model: its structure in HLL, its behavior in sHLL. Where the UML 2.5 semantics leave room for interpretation, for example in how events are queued, the choice we make is kept explicit and checked as its own property.

We then check four groups of properties with Prover PSL: rules from the UML and EULYNX standards, quality properties such as reachability and determinism, the translator’s own design choices, and, as a next step, safety properties derived from hazards. All 18 state machines of the Point subsystem and the SCI-RBC interface passed the automatic and structural checks without manual intervention. Along the way, the work made open points in the standards explicit and caught specification defects in other EULYNX subsystems, all to be reported to EULYNX.

Formal Verification and Testing of EULYNX Specifications

The second talk, in the DisCoRail track, took the next step: composing the state machines into one formal model per EULYNX subsystem, and using that one model for three things.

• Verification: prove properties of the specification with Prover PSL, starting with determinism.
• Test execution: run the official EULYNX test cases on the model.
• Test generation: derive new test cases from coverage objectives, delivered in the format of the EULYNX test-case catalog.

The translation has been applied to six subsystems and two external interfaces, with Point and SCI-RBC analyzed in detail. Three findings stand out. First, the composed models are non-deterministic: two implementations can each be deterministic and conformant, yet incompatible with each other. Second, some official Point test cases can accept faulty behavior, because what they actually check is weaker than what their description says. Third, the translation and structural checks caught specification defects. All of them will be reported to EULYNX.

Architectural Variants of ETCS-Based Trackside Systems in a Unified Ontology-Driven Validation Framework

In the third talk, Arne Borälv, with Daniel Schwencke of DLR, looked at where trackside systems are heading. Today’s ETCS Level 2 ties routes in the interlocking tightly to movement authority in the radio block center. Moving block, hybrid train detection and initiatives such as RCA and Europe’s Rail System Pillar push towards more varied, train-centric architectures. A model that hard-codes one architecture has to be rebuilt for every variant, and its tests and proofs cannot be shared.

The paper shows another way: keep a stable, train-centric core of concepts, generated from a layered ontology, and express each architecture as constraints on top of it. Moving block, fixed block, hybrid and dynamic-route variants all fit the same model, so tests and formal properties are defined once and reused.

Because the variants differ only in their constraints, they can also be compared side by side in one environment: how each set of constraints shapes what trains are allowed to do, how their safety properties compare, and where the balance between flexibility and restriction lies. Directions for further work include formalizing the refinement itself, with a focus on preserving safety properties, and a closer look at the interfaces between components such as the interlocking and the RBC. The work was carried out in Europe’s Rail project FP2-R2DATO.

About ForTeS

ForTeS is funded by DZSF and carried out with DLR and ESE. It develops verification and testing methods for EULYNX subsystems; Prover’s part covers formalizing the specifications, formal verification and test generation.

Thanks to the ISoLA organizers and the ScaIVeri and DisCoRail track chairs, and to everyone who came by with questions.

Want to know more about any of the papers? Get in touch with us.