The European Railway Traffic Management System (ERTMS) aims at the replacement of incompatible national railway traffic management systems in Europe. A part of ERTMS is the European Train Control System (ETCS). ETCS is an automatic train protection system and can collaborate with an automatic train operation system (ATO). ATO can control and monitor the braking, traction and door system of a train. This collaboration is called ATO over ETCS. In this paper we describe the experiences gained in the formalization and the formal analysis of system requirements related to the modes of the ATO onboard unit and its interfaces to train, ATO trackside unit, and ETCS onboard unit. A primary goal to achieve was the stepwise and systematic construction of an Event-B specification tightly coupled with the requirements based on a bidirectional traceability concept. Another goal was the formal verification of important safety properties related to the mode transitions and transition conditions of the ATO onboard unit.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Eschbach21,
author = {Robert Eschbach},
editor = {Alexander Raschke and
Dominique M{\'{e}}ry},
title = {Formalizing and Analyzing System Requirements of Automatic Train Operation
over {ETCS} Using Event-B},
booktitle = {Rigorous State-Based Methods - 8th International Conference, {ABZ}
2021, Ulm, Germany, June 9-11, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12709},
pages = {137--142},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-77543-8\_13},
doi = {10.1007/978-3-030-77543-8\_13},
timestamp = {Tue, 15 Jun 2021 17:24:03 +0200},
biburl = {https://dblp.org/rec/conf/asm/Eschbach21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}