Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems
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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-11-01
|
| Series: | Energies |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1996-1073/15/23/9041 |
| _version_ | 1797463277875232768 |
|---|---|
| author | Juliusz Karolak Wiktor B. Daszczuk Waldemar Grabski Andrzej Kochan |
| author_facet | Juliusz Karolak Wiktor B. Daszczuk Waldemar Grabski Andrzej Kochan |
| author_sort | Juliusz Karolak |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-03-09T17:48:26Z |
| format | Article |
| id | doaj.art-6bd09076f09b46779dcb441a5248e1be |
| institution | Directory Open Access Journal |
| issn | 1996-1073 |
| language | English |
| last_indexed | 2024-03-09T17:48:26Z |
| publishDate | 2022-11-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Energies |
| spelling | doaj.art-6bd09076f09b46779dcb441a5248e1be2023-11-24T10:54:29ZengMDPI AGEnergies1996-10732022-11-011523904110.3390/en15239041Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed SystemsJuliusz Karolak0Wiktor B. Daszczuk1Waldemar Grabski2Andrzej Kochan3Faculty of Transport, Warsaw University of Technology, Koszykowa Str. 75, 00-662 Warszawa, PolandInstitute of Computer Science, Warsaw University of Technology, Nowowiejska Str. 15/19, 00-665 Warszawa, PolandInstitute of Computer Science, Warsaw University of Technology, Nowowiejska Str. 15/19, 00-665 Warszawa, PolandFaculty of Transport, Warsaw University of Technology, Koszykowa Str. 75, 00-662 Warszawa, PolandRelay-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.https://www.mdpi.com/1996-1073/15/23/9041railway traffic control safetyrelay-based railway traffic control systems modelingrailway traffic control system verificationintegrated model of distributed systemsmodel checking |
| spellingShingle | Juliusz Karolak Wiktor B. Daszczuk Waldemar Grabski Andrzej Kochan Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems Energies railway traffic control safety relay-based railway traffic control systems modeling railway traffic control system verification integrated model of distributed systems model checking |
| title | Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems |
| title_full | Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems |
| title_fullStr | Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems |
| title_full_unstemmed | Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems |
| title_short | Temporal Verification of Relay-Based Railway Traffic Control Systems Using the Integrated Model of Distributed Systems |
| title_sort | temporal verification of relay based railway traffic control systems using the integrated model of distributed systems |
| topic | railway traffic control safety relay-based railway traffic control systems modeling railway traffic control system verification integrated model of distributed systems model checking |
| url | https://www.mdpi.com/1996-1073/15/23/9041 |
| work_keys_str_mv | AT juliuszkarolak temporalverificationofrelaybasedrailwaytrafficcontrolsystemsusingtheintegratedmodelofdistributedsystems AT wiktorbdaszczuk temporalverificationofrelaybasedrailwaytrafficcontrolsystemsusingtheintegratedmodelofdistributedsystems AT waldemargrabski temporalverificationofrelaybasedrailwaytrafficcontrolsystemsusingtheintegratedmodelofdistributedsystems AT andrzejkochan temporalverificationofrelaybasedrailwaytrafficcontrolsystemsusingtheintegratedmodelofdistributedsystems |