FormaSig: Formal methods in railway signalling infrastructure standardisation processes

Funded by: ProRail; DB Netze A.G.
Duration: March 2019 until June 2023
Contact: Prof.dr. M.I.A. Stoelinga

Summary of the project

European railroad infrastructure managers have joined forces in the EULYNX organisation with the aim to arrive at standardised interfaces between interlockings and trackside equipment. Standardisation efforts will significantly reduce the cost of ownership of signalling systems. Indeed, if the interfaces and architecture of a signalling system are standardised, then different components can be procured from different suppliers, thereby enabling competition and preventing vendor lock-in situations. Furthermore, approval processes can be harmonised and simplified, and will thus become more efficient.

The goal of the FormaSig project is to formally verify these interfaces, and check compliance with the standard, so that delivered products satisfy certain properties. Using the formal model, it can also be more thoroughly tested whether a delivered component complies with the standard (formal model-based testing). Furthermore, the application of formal verification techniques will help to validate to what extent the standard guarantees national requirements and they will help to improve tender documents. We could, e.g., also make a formal model of the national requirements and then conduct a thorough mathematical comparison with the formal model of the standard, and test cases derived from the formal model of the standard could be included in tender documents.

In this project, Twente University collaborates with Eindhoven University of Technology, ProRail, and DB Netze A.G.

Involved people are

Djurre van der Wal (Twente University)
Mariëlle Stoelinga (Twente University)
Arend Rensink (Twente University)
Mark Bouwman (Eindhoven University of Technology)
Bas Luttik (Eindhoven University of Technology)
Maarten van der Werff (ProRail)
Daan van der Meij (ProRail)