https://www.mdu.se/

The European Train Control System Level 3 (ETCS-L3) leverages continuous communication and precise train localization to optimize traffic management and enhance safety. This paper presents a formal modeling approach for the control of railway switches within the ETCS-L3 framework. Formal methods enable the development of precise and verifiable models to ensure the correctness of switch operations, essential for train routing and collision avoidance. The work is part of the PERFORMINGRAIL project, integrating advanced formal verification tools and techniques to facilitate rigorous analysis and validation. The project also explores model diversity in moving block systems' safety and performability analysis. This paper specifically focuses on the control logic of railway switches, capturing the behavior of the point control subsystem and leveraging various modeling approaches. The switch control models address various operational scenarios, including normal operations, failure modes, and recovery procedures. The findings show that formal methods can significantly improve the robustness of railway switch systems, thereby contributing to safer and more efficient railway networks. This work paves the way for future research and implementation of formalized control systems in the broader context of smart and autonomous railway operations.