No Cover Image

Journal article 241 views 25 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, Volume: 154, Pages: 61 - 88

Swansea University Author: James, Phillip

  • 39973.pdf

    PDF | Accepted Manuscript

    Released under the terms of a Creative Commons Attribution Non-Commercial No Derivatives License (CC-BY-NC-ND).

    Download (583.29KB)

Abstract

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 traditional discrete interlocking systems and aims at improving performance and capacity of rail traffic systems without compromising their...

Full description

Published in: Science of Computer Programming
ISSN: 01676423
Published: 2018
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa39973
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: 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 traditional discrete interlocking systems and aims at improving performance and capacity of rail traffic systems without compromising their safety. The ERTMS system is of hybrid nature, consequently, the switch to ERTMS poses a number of research questions to the formal methods community, most prominently: How can safety be guaranteed? In this paper we present the first formal modelling of ERTMS comprising all subsystems participating in its control cycle. We capture what safety means in physical and in logical terms, and we demonstrate that it is feasible to prove safety of ERTMS systems utilising Real-Time Maude model-checking by considering a number of bi-directional track layouts.
Keywords: Railway signalling, ERTMS/ETCS, Hybrid systems, Real-Time Maude, Model-checking
College: College of Science
Start Page: 61
End Page: 88