ERTMS
The European Rail Traffic Management System (ERTMS) is a system of standards for management and interoperation of signalling for railways by the EU, that aims to replace the various national systems with a seamless European railway system. The European Train Control System (ETCS), the ERTMS control command part, defines 3 levels of signalling that a system can operate on, depending on on the trackside equipment used, how the on-board systems communicate with the trackside, and on which functions are processed on-board or by the trackside.
In Level 3, positive train detection (PTD) information is detected and reported by the on-board system directly to the trackside, which, based on logical rather than physical track block sections, decides whether it is safe to issue movement authorities (MA), reporting them back to the on-board system via radio. For this to be feasible, PTD information must be reliable and the communication between the on-board and the trackside systems guaranteed at all times. These pre-conditions are not easily met, which has led to the proposal of a Hybrid Level 3 concept, that combines PTD information with limited trackside detection. These trackside train detection sections (TTD) are then broken into smaller virtual subsections (VSS). This allows for trains with non-ideal equipment or with communication problems to still use the line, albeit below full capacity.
This page presents the modelling and subsequent validation and verification of the Hybrid ERTMS/ETCS Level 3 (HL3) concept in Electrum, and was developed as an answer to the ABZ 2018 call for case study contributions, mainly based on the detailed HL3 principles document.
The Electrum model for the HL3 concept is present in detail in the ABZ 2018 publication. The model at the time of the conference, for version 1A of the reference document, is available here (with the respective theme here). A version of the model in plain Alloy was also developed, available here (with the respective theme here). A new version of the reference document was released for publication of the conference. The model for this 1C version is also available here (with the respective theme here), and is described in the extended version of the paper at STTT.
Note: While these models were initially developed for Electrum 1.1, they have been updated for Electrum 2.1 in order to be analysable by the latest version of the tool.
The 9 operational scenarios provided by the HL3 principles document, generated by the Electrum Analyzer for this model, are presented below.
 |
 |
 |
 |
| Disconnected train | Connected train not reporting | Connected train not reporting rear info | Connected train fully reporting |
 |
 |
 |
 |
| Train with expired mute timer | Train with expired integrity timer | Actual train front position | Actual train rear position |
 |
 |
 |
 |
| Free VSS | Occupied VSS | Ambiguous VSS | Unknown VSS |
 |
 |
 |
 |
| VSS with expired disconnected propagation timer | VSS with expired integrity loss propagation timer | MA assigned to a train | Jumping train info |
 |
 |
 |
 |
| Free TTD | Occupied TTD | TTD with expired shadow timer A | TTD with expired shadow timer B |
 |
 |
||
| TTD with expired ghost propagation timer | VSSs comprising a TTD |
