Disclaimer: FormaSig is fully funded by ProRail and DB Netz AG, but the vision presented here does not necessarily reflect the strategy of DB Netz AG or ProRail.

The main goal of the FormaSig project is to develop a formal method to support railway standardisation projects, in particular EULYNX. It is a collaboration between the Formal System Analysis research group at Eindhoven University of Technology, the Formal Methods and Tools research group at University of Twente, and the Dutch and German railway infrastructure managers ProRail and DB Netze. The project employs two PhD students.

The aim of EULYNX is to arrive at standardised interfaces between interlockings and trackside equipment (signals, points, level crossings). 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 main ideas of the FormaSig project.

It is crucial that the EULYNX standard is unambiguous, that it ensures all relevant safety requirements, and that compliance to interfaces to the EULYNX standard can be tested thoroughly. The FormaSig project will deliver a method by which the quality of the standard can be formally analysed and compliance to the standard can be tested.

EULYNX defines the standardised interfaces through SysML models. The approach of FormaSig is to automatically derive, from these SysML models, a formal model in the process specification language mCRL2. This mCRL2 model will be central. It can, on the one hand, be used to formally and exhaustively analyse the correctness of the interface model with respect to high-level safety requirements. On the other hand, model can be used to automatically test compliance to the standard of delivered components. The latter will be done by in accordance with formal testing theory, automatically deriving test cases from the mCRL2 model.

For more information, please contact Bas Luttik.

Academics involved: