IDEAS home Printed from https://ideas.repec.org/a/gam/jeners/v16y2023i8p3602-d1129571.html
   My bibliography  Save this article

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

Author

Listed:
  • 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)

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.

Suggested Citation

  • Andrzej Kochan & Wiktor B. Daszczuk & Waldemar Grabski & Juliusz Karolak, 2023. "Formal Verification of the European Train Control System (ETCS) for Better Energy Efficiency Using a Timed and Asynchronous Model," Energies, MDPI, vol. 16(8), pages 1-22, April.
    • Handle: RePEc:gam:jeners:v:16:y:2023:i:8:p:3602-:d:1129571
    as

    Download full text from publisher

    File URL: https://www.mdpi.com/1996-1073/16/8/3602/pdf
    Download Restriction: no
    File URL: https://www.mdpi.com/1996-1073/16/8/3602/
    Download Restriction: no
    ---><---

    References listed on IDEAS

    as
    1. Juliusz Karolak & Wiktor B. Daszczuk & Waldemar Grabski & Andrzej Kochan, 2022. "Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems," Energies, MDPI, vol. 15(23), pages 1-22, November.
    2. Janusz Szkopiński & Andrzej Kochan, 2021. "Energy Efficiency and Smooth Running of a Train on the Route While Approaching Another Train," Energies, MDPI, vol. 14(22), pages 1-27, November.
    3. Emilia Koper & Andrzej Kochan, 2020. "Testing the Smooth Driving of a Train Using a Neural Network," Sustainability, MDPI, vol. 12(11), pages 1-14, June.
    Full references (including those not matched with items on IDEAS)

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Janusz Szkopiński & Andrzej Kochan, 2023. "Maximization of Energy Efficiency by Synchronizing the Speed of Trains on a Moving Block System," Energies, MDPI, vol. 16(4), pages 1-26, February.
    2. Marek Stawowy & Adam Rosiński & Jacek Paś & Stanisław Duer & Marta Harničárová & Krzysztof Perlicki, 2023. "The Reliability and Exploitation Analysis Method of the ICT System Power Supply with the Use of Modelling Based on Rough Sets," Energies, MDPI, vol. 16(12), pages 1-18, June.
    3. Janusz Szkopiński & Andrzej Kochan, 2021. "Energy Efficiency and Smooth Running of a Train on the Route While Approaching Another Train," Energies, MDPI, vol. 14(22), pages 1-27, November.
    4. Wolfram Heineken & Marc Richter & Torsten Birth-Reichert, 2023. "Energy-Efficient Train Driving Based on Optimal Control Theory," Energies, MDPI, vol. 16(18), pages 1-40, September.
    5. Manuel Blanco-Castillo & Adrián Fernández-Rodríguez & Antonio Fernández-Cardador & Asunción P. Cucala, 2022. "Eco-Driving in Railway Lines Considering the Uncertainty Associated with Climatological Conditions," Sustainability, MDPI, vol. 14(14), pages 1-26, July.

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:gam:jeners:v:16:y:2023:i:8:p:3602-:d:1129571. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: MDPI Indexing Manager (email available below). General contact details of provider: https://www.mdpi.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.