Keywords

1 ATO over ETCS

The European Railway Traffic Management System (ERTMS) aims at the replacement of incompatible national railway traffic management systems in Europe. A central part of ERTMS is ETCS. In this paper we will focus on the collaboration of ETCS with ATO called ATO over ETCS (AoE). The system requirements for ATO over ETCS (AoE) have been specified within the Shift2Rail research project X2RAIL-1. Further information can be obtained from https://projects.shift2rail.org (accessed Feb 11, 2021). The system requirements are specified in SUBSET-125Footnote 1. As can be seen in the reference architecture of AoE depicted in Fig. 1 the ATO is divided in ATO onboard unit (ATO-OB) and ATO trackside unit (ATO-TS). The following ATO-OB interface specifications have been analyzed: ATO-TS (SUBSET-125), ETCS onboard unit (ETCS-OB) (SUBSET-130, SUBSET-143) and Train (SUBSET-139). A main part of the system requirements is related to ATO-OB operation modes and mode transitions (see Fig. 2).

Fig. 1.
figure 1

AoE reference architecture

Full size image

Related Work. Formal methods have been applied to ETCS in several research and industrial projects. For example, in [9] the authors designed a controller for a cooperation protocol of control parameters. They identified constraints in order to ensure collision freedom. In [7] a concrete implementation of the ETCS Hybrid Level 3 concept is presented. The authors introduce so called virtual block functions which computes the occupation states of virtual subsections. In [3] the authors describe the experiences gained in modelling a satellite-based ERTMS L3 moving block signalling system with Simulink and Uppaal and analysing the Uppaal model with the statistical model checker Uppaal SMC. In [5] the authors present a proof of concept of Virtual coupling. They introduce a specific operating mode for ETCS and define a coupling control algorithm that addresses time-varying delays affecting the communication links. In [1] the authors model the principles of ERTMS Hybrid Level 3 in the mCRL2 process algebra. They perform an analysis with the mCRL2 toolset which can be used for modelling, validation and verification of concurrent systems and protocols. The identified issues have been communicated to the EEIG ERTMS Users Group and have led to several improvements of the affected specifications. In [4] the authors present a detailed report on the convergence of FM related studies carried out in the Shift2Rail projects X2Rail-2 and ASTRail. In both projects a systematic survey of the state of the art of formal methods application in railway industry and related best practices was carried out. In [2] the authors present the results of a questionnaire which was part of the analysis phase of ASTRail research project. One of the most important results is that classical B and Event-B with the respective tools Atelier-B, ProB and Rodin were used most often in projects.

The formalization approach described in this paper consists of the following six steps (1) identify components, (2) derive function tables for relevant requirements, (3) derive a variable table with read/write permissions for the identified components, (4) derive Event-B specification, (5) validation, and (6) verification.

Fig. 2.
figure 2

AoE mode transitions (excerpt)

Full size image

Step 1: Identify Components. The first step in the formal analysis consists of the systematic identification of components and boundaries specified in SUBSET-125. The ATO-OB is the main component whereas in the environment of ATO-OB the following components were identified: ATO-TS, ETCS-OB, Driver and Train.

Step 2: Derive Function Tables. The formalization started with the stepwise extraction of conditions and actions related to modes like ATO Engaged of the ATO-OB and its related mode transitions and transition conditions. For each mode all conditions and actions were combined in a so-called function table as proposed by Dave Parnas (for example [8]). Function tables and Event-B were successfully applied in [6]. Traceability information was added to conditions and actions that allows for relating requirements with elements of the function tables. Furthermore, a coverage analysis was made in order to ensure that all relevant requirements have been covered by the analysis. In Fig. 3 an excerpt of function table for ATO-OB mode ATO Ready (RE) is depicted.

Fig. 3.
figure 3

AoE function table for ATO-OB mode ready (excerpt)

Full size image

Each function table consists of a hierarchical structured condition block, a value block and a variable block. Each column describes an event that consist of the conjunction of all conditions which are part of the column and an action which assigns in parallel all column values to the variables. Each column has been later formalized to an event of the corresponding Event-B specification. The trace to this event is specified in the first row of the function table. In this way a bidirectional traceability between function table and events of the Event-B specification is established.

Step 3: Derive Variable Table. The next analysis step consists of identifying variables in the conditions and actions so that conditions and actions can be reformulated formally. The requirements were analyzed such that types (like bool or enumeration types) can be assigned to the variables. This involves the analysis of relevant interface specifications, especially the interface between ATO-OB and ETCS-OB and the interface between ATO-OB and train, respectively. Based on this analysis, for each variable and for each component read/write permissions were assigned. In addition, traceability information related to both the interface and system requirements and events of the Event-B specification was added. For example, variable ato_ob_etcs_ob_in_ad_mode with type bool is defined. The justification for this decision is given by the trace [130, 7.3.2.2] [9.10.8, 10>-p3-] pointing to section 7.3.2.2 of SUBSET-130 and to transition 10 (with priority 3) in section 9.1.8 of SUBSET-125. SUBSET-130 defines a signal with name Q_ADMODE which can take the values 0 or 1. The ETCS-OB will send this signal cyclically to the ATO-OB (indicating whether it is in AD mode or not). The component ATO-OB has read permission, the environment component ETCS-OB has write permission. All other environment components have neither read nor write permissions.

Step 4: Derive Event-B Specification. The derived Event-B Specification has 25 variables, 30 invariants and 41 events. In Fig. 4 event \(\texttt {ato\_ob\_mode\_re\_6}\) (excerpt) is shown which has been derived from column \(\texttt {[ato\_ob\_mode\_re\_6]}\) of the function table depicted in Fig. 3.

Fig. 4.
figure 4

Event ato_ob_mode_re_6

Full size image

Step 5: Validation. In SUBSET-125 several scenarios of AoE are specified. These scenarios are classified as descriptions (they are not requirements). For example, section 9.10.2 describes the nominal scenario in which the ATO will be engaged by the driver for each so-called journey segment. We have used ProB for simulating step-by-step these scenarios in order to validate the model.

Step 6: Verification. The formal verification was mainly done by theorem proving with the tool Rodin and the Atelier B prover, the SMT solvers and ProB plugins. Furthermore, refinement steps were used to impose further constraints on the environment. For example, since AoE realizes so-called Grade of Automation level 2, a very important safety property is that ATO will never be engaged when the driver never selects ATO Engage. In a refinement step the behavior of the driver was constrained such that he can never select ATO Engage. It was proven that an ATO-OB in this refined Event-B specification is never in mode ATO Engaged (EG) or ATO Disengaging (DE) (the only modes in which ATO is engaged).

Conclusion. In this paper the experiences gained in the formalisation and analysis of AoE was presented. The formal analysis of the mode transition requirements revealed 23 ambiguities and missing requirements. The formal analysis will be continued in the future. According to the determined refinement strategy the focus will be on the important functional layers ATO Active Functions Table and ETCS mode transition requests (SUBSET-125, 9.11, 9.12), respectively. With these refinement steps the functional layer ATO Operational States (SUBSET-125, 9) will be completely addressed.