Formal Verification of the European Train Control System (ETCS) for Better Energy Efficiency Using a Timed and Asynchronous Model

Andrzej Kochan (), Wiktor B. Daszczuk, Waldemar Grabski and Juliusz Karolak
Additional contact information
Andrzej Kochan: Faculty of Transport, Warsaw University of Technology, 00-662 Warsaw, Poland
Wiktor B. Daszczuk: Institute of Computer Science, Warsaw University of Technology, 00-665 Warszawa, Poland
Waldemar Grabski: Institute of Computer Science, Warsaw University of Technology, 00-665 Warszawa, Poland
Juliusz Karolak: Faculty of Transport, Warsaw University of Technology, 00-662 Warsaw, Poland

Energies, 2023, vol. 16, issue 8, 1-22

Abstract: The ERTMS/ETCS is the newest automatic train protection system. This is a system that supports the driver in driving the train. It is currently being implemented throughout the European Union. This system’s latest specifications also provide additional functions to increase the energy efficiency of train driving in the form of ATO (automatic train operation). These functions of the ETCS will be valuable, provided they operate without failure. To achieve errorless configuration of the ETCS, a methodology for automatic system verification using the IMDS (Integrated Model of Distributed Systems) formalism and the temporal tool Dedan was applied. The main contribution is asynchronous and timed verification, which appropriately models the distributed nature of the ETCS and allows the designer not only to analyze time dependencies but also to define the range of train velocities in which the operational scenario is valid. Additionally, the novelties of the presented verification methodology are the graphical design of the system components and automated verification freeing the designer from using textual design. We express the verified properties as observer automata rather than in temporal logic. Moreover, we check partial properties related to system fragments, which is crucial in distributed systems. This paper presents the verification of an example ETCS system application. The verification results are presented as sequence diagrams leading to a correct/incorrect final state.

Keywords: energy efficiency of train operation; ETCS system verification; timed integrated model of distributed systems; timed model checking; asynchronous modeling; energy efficiency (search for similar items in EconPapers)
JEL-codes: Q Q0 Q4 Q40 Q41 Q42 Q43 Q47 Q48 Q49 (search for similar items in EconPapers)
Date: 2023
References: View references in EconPapers View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
https://www.mdpi.com/1996-1073/16/8/3602/pdf (application/pdf)
https://www.mdpi.com/1996-1073/16/8/3602/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jeners:v:16:y:2023:i:8:p:3602-:d:1129571

Access Statistics for this article

Energies is currently edited by Ms. Agatha Cao

More articles in Energies from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().