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

Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems

Author

Listed:
  • Juliusz Karolak

    (Faculty of Transport, Warsaw University of Technology, Koszykowa Str. 75, 00-662 Warszawa, Poland)

  • Wiktor B. Daszczuk

    (Institute of Computer Science, Warsaw University of Technology, Nowowiejska Str. 15/19, 00-665 Warszawa, Poland)

  • Waldemar Grabski

    (Institute of Computer Science, Warsaw University of Technology, Nowowiejska Str. 15/19, 00-665 Warszawa, Poland)

  • Andrzej Kochan

    (Faculty of Transport, Warsaw University of Technology, Koszykowa Str. 75, 00-662 Warszawa, Poland)

Abstract

Relay-based traffic control systems are still used in railway control systems. Their correctness is most often verified by manual analysis, which does not guarantee correctness in all conditions. Passenger safety, control reliability, and failure-free operation of all components require formal proof of the control system’s correctness. Formal evidence allows certification of control systems, ensuring that safety will be maintained in correct conditions and the in event of failure. The operational safety of systems in the event of component failure cannot be manually checked practically in the event of various types of damage to one component, pairs of components, etc. In the article, we describe the methodology of automated system verification using the IMDS (integrated model of distributed systems) temporal formalism and the Dedan tool. The novelty of the presented verification methodology lays in graphical design of the circuit elements, automated verification liberating the designer from using temporal logic, checking partial properties related to fragments of the circuit, and fair verification preventing the discovering of false deadlocks. The article presents the verification of an exemplary relay traffic control system in the correct case, in the case of damage to elements, and the case of an incorrect sequence of signals from the environment. The verification results are shown in the form of sequence diagrams leading to the correct/incorrect final state.

Suggested Citation

  • 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.
    • Handle: RePEc:gam:jeners:v:15:y:2022:i:23:p:9041-:d:988163
    as

    Download full text from publisher

    File URL: https://www.mdpi.com/1996-1073/15/23/9041/pdf
    Download Restriction: no
    File URL: https://www.mdpi.com/1996-1073/15/23/9041/
    Download Restriction: no
    ---><---

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. 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.
    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.

    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:15:y:2022:i:23:p:9041-:d:988163. 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.

    We have no bibliographic references for this item. You can help adding them by using 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.