Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6875285 | Science of Computer Programming | 2018 | 28 Pages |
Abstract
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 the event-response structures present in the ERTMS. Then, we model these structures in Real-Time Maude in a traceable way, i.e., specification text in Real-Time Maude can be directly mapped to requirements. We explore our models by checking if they have the 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 railway domain, and we mathematically prove that our analysis of ERTMS by model-checking is complete, i.e., that it guarantees safety at all times.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ulrich Berger, Phillip James, Andrew Lawrence, Markus Roggenbach, Monika Seisenberger,