Verification of the European Rail Traffic Management System in Real-Time Maude
- Submitting institution
-
Swansea University / Prifysgol Abertawe
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 37102
- Type
- D - Journal article
- DOI
-
10.1016/j.scico.2017.10.011
- Title of journal
- Science of Computer Programming
- Article number
- -
- First page
- 61
- Volume
- 154
- Issue
- -
- ISSN
- 0167-6423
- Open access status
- Compliant
- Month of publication
- March
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 7
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The European Rail Traffic Management System (ERTMS) is a state-of-the-art train control system and is the main standard for the foreseeable future. Rail industry proposed the challenge of modelling and formally verifying all ERTMS components in one system. This is the first paper to present a formal modelling of ERTMS comprising all subsystems participating in its control cycle and to prove its safety. Furthermore, we are the first to establish Real-Time Maude as applicable to the railway-domain by modelling and verifying a real-world ERTMS system. The work is central to Swansea’s Railway Verification group who submitted an impact case study.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -