Repository migration notice
This repository is no longer actively maintained.
Ongoing development and updates have been moved to the following GitLab repository:
👉 https://gitlab.univ-eiffel.fr/julie.beugin/ETCS-Moving-Block-System
This repository hosts formal behavioural models and verification artefacts supporting research on the safety of ETCS Moving Block railway systems.
The work extends modelling previously initiated in PERFORMINGRAIL (2020–2023) and is aligned with the Shift2Rail X2Rail-1, X2Rail-3, and X2Rail-5 functional specifications.
This research is conducted within the "Safety of Railway Systems" Chair, funded by Certifer.
The repository evolves progressively and includes artefacts associated with related publications:
- ICSRS 2025: Araaf Recta, Rim Saddem-Yagoubi, Julie Beugin, Mohamed Ghazel,"Formal Modeling of Advanced Railway Route Management with Moving Blocks - A Property-Oriented Approach," in ICSRS 2025, the 9th International Conference on System Reliability and Safety – IEEE, Turin, Italy, November 26-28, 2025 (The artefacts provided correspond to the components relevant to the ICSRS paper. The fully integrated PERFORMINGRAIL-based modules will be shared in future publications)
- Formalisms: Timed automata
- Verification tool: UPPAAL
These artefacts are intended for academic and research use.
If you reuse or extend these materials, please cite the corresponding publications (see list above).
License: CC BY-4.0