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.
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:
- Mark Bouwman (PhD student)
- Djurre van der Wal (PhD student)
- Bas Luttik (contact person)
- Arend Rensink
- Marielle Stoelinga
Publications:
- Mark Bouwman. Supporting Railway Standardisation with Formal Verification. PhD Thesis, Eindhoven University of Technology, 2023.
- Mark Bouwman, Djurre van der Wal, Bas Luttik, Marielle Stoelinga and Arend Rensink. A Case in Point: Verification and Testing of a EULYNX Interface. Formal Aspects of Computing 35(1:2):1-38, 2023.
- Mark Bouwman, Bas Luttik, Arend Rensink, Marielle Stoelinga and Djurre van der Wal. Formal Methods in Railway Signalling Infrastructure Standardisation Processes. In: Tiziana Margaria and Bernhard Steffen, editors, Proceedings ISoLA 2021, LNCS 13036, pp. 500-501, 2021 (see Back Matter).
- Mark Bouwman, Bas Luttik and Djurre van der Wal. A Formalisation of SysML State Machines in mCRL2. In: K. Peters and T.A.C. Willemse, editors, Proceedings FORTE 2021, LNCS 12719, pp. 42-59, 2021.
- Mark Bouwman, Djurre van der Wal, Bas Luttik, Marielle Stoelinga and Arend Rensink. What is the Point: Formal Analysis and Test Generation for a Railway Standard. In: Piero Baraldi, Francesco Di Maio and Enrico Zio, editors, Proceedings of the 30th European Safety and Reliability Conference and the 15th Probabilistic Safety Assessment and Management Conference (ESREL 2020 PSAM 15), pp. 921-928, Research Publishing, Singapore, 2020.
- Maarten van der Werff, Bernd Elsweiler, Bas Luttik and Paul Hendriks. The use of formal methods in standardisation of interfaces of signalling systems. IRSE News 256, pp. 15-17, June 2019.