A4 Refereed article in a conference publication
Railway Switch Control Modeling in European Train Control System Level 3
Authors: Flammini, Francesco; Marrone, Stefano; Nardone, Roberto; Sanwal, Usman; Seceleanu, Cristina; Verde, Laura; Vittorini, Valeria
Editors: Margaria, Tiziana; Steffen, Bernhard
Conference name: International Symposium on Leveraging Applications of Formal Methods
Publisher: SPRINGER INTERNATIONAL PUBLISHING AG
Publishing place: CHAM
Publication year: 2025
Journal: Lecture Notes in Computer Science
Book title : Leveraging Applications of Formal Methods, Verification and Validation. Application Areas: 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part V
Journal acronym: LECT NOTES COMPUT SC
Series title: Lecture Notes in Computer Science
Volume: 15223
First page : 174
Last page: 189
Number of pages: 16
ISBN: 978-3-031-75389-3
eISBN: 978-3-031-75390-9
ISSN: 0302-9743
eISSN: 1611-3349
DOI: https://doi.org/10.1007/978-3-031-75390-9_12
Web address : https://doi.org/10.1007/978-3-031-75390-9_12
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.