Journal article 252 views 13 downloads
Verification of the European Rail Traffic Management System in Real-Time Maude / Ulrich Berger; Phillip James; Andrew Lawrence; Markus Roggenbach; Monika Seisenberger
Science of Computer Programming
Swansea University Author: Seisenberger, Monika
PDF | Accepted Manuscript
© 2017. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/Download (583.26KB)
The European Rail Traffic Management System (ERTMS) is a state-of-the-art train control system designed as a standard for railways across Europe. It generalises traditionaldiscrete interlocking systems to a world in which trains hold on-board equipment forsignalling, and trains and interlockings com...
|Published in:||Science of Computer Programming|
Check full text
No Tags, Be the first to tag this record!
The European Rail Traffic Management System (ERTMS) is a state-of-the-art train control system designed as a standard for railways across Europe. It generalises traditionaldiscrete interlocking systems to a world in which trains hold on-board equipment forsignalling, and trains and interlockings communicate via radio block processors. TheERTMS aims at improving performance and capacity of rail traffic systems withoutcompromising their safety.The ERTMS system is of hybrid nature, in contrast to classical railway signallingsystems which deal with discrete data only. Consequently, the switch to ERTMS poses anumber of research questions to the formal methods community, most prominently: Howcan safety be guaranteed? In this paper we present the first formal modelling of ERTMScomprising all subsystems participating in its control cycle. We capture what safetymeans in physical and in logical terms, and we demonstrate that it is feasible to provesafety of ERTMS systems utilising Real-Time Maude model-checking by considering anumber of bi-directional track layouts.ERTMS is currently being installed in many countries. It will be the main traincontrol standard for the foreseeable future. The concepts presented in this paper offerapplicable methods supporting the design of dependable ERTMS systems. We demon-strate model-checking to be a viable option in the analysis of large and complex real-timesystems. Furthermore, we establish Real-Time Maude as a modelling and verificationtool applicable to the railway domain.The approach given in this paper is a rigorous one. In order to avoid modelling errors,we follow a systematic approach: First, as a requirement specification, we identify theevent-response structures present in the ERTMS. Then, we model these structures inReal-Time Maude in a traceable way, i.e., specification text in Real-Time Maude canbe directly mapped to requirements. We explore our models by checking if they havethe desired behaviour, and apply systematic model-exploration through error injection– both these steps are carried out using the formal method Real-Time Maude. Finally,we analyse ERTMS by model-checking, thus applying a formal method to the railwaydomain, and we mathematically prove that our analysis of ERTMS by model-checking iscomplete, i.e., that it guarantees safety at all times.
College of Science