Author(s)

ROBERT ESCHBACH

Abstract

The European Railway Traffic Management System (ERTMS) is intended to replace incompatible national rail traffic management systems in Europe and thus simplify cross-border rail traffic. 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 integrated application of the model-based systems and architecture engineering method ARCADIA and the formal method Event-B to the system requirements of ATO over ETCS. A central part of the system requirements is related to the operational modes, mode transitions and mode properties of the ATO onboard unit (ATO-OB). Mode properties are system requirements that must be satisfied whenever the ATO-OB enters a mode or stays within a mode. Especially modes, in which the ATO-OB automatically drives the train, are of utter importance. The main goal of the analysis was to check consistency and completeness of the system requirements related to modes, mode transitions and mode properties. Within the ARCADIA phase “System Analysis” a socalled “Mode/State Model”, a special ARCADIA model, was systematically derived from the system requirements. In order to guarantee consistency, especially to guarantee that mode properties will not be violated by mode transitions, a formal Event-B specification was derived and formally analyzed. This analysis approach identified several critical inconsistencies of the system requirements.

Keywords

ATO over ETCS, MBSE, formal methods, ARCADIA, Event-B