Verification of Railway Control Systems Using Model Checking and CTL, Explained Through a Case Study

Authors

  • Gábor Lukács
    Affiliation
    Department of Control for Transportation and Vehicle Systems, Faculty of Transportation Engineering and Vehicle Engineering, Budapest University of Technology and Economics, Műegyetem rkp. 3., H-1111 Budapest, Hungary
  • Tamás Bartha
    Affiliation
    Department of Control for Transportation and Vehicle Systems, Faculty of Transportation Engineering and Vehicle Engineering, Budapest University of Technology and Economics, Műegyetem rkp. 3., H-1111 Budapest, Hungary Institute for Computer Science and Control (SZTAKI), Kende street 13-17., H-1111 Budapest, Hungary
https://doi.org/10.3311/PPtr.23344

Abstract

Systematic faults can often occur during the development of a system. The later such faults are discovered, the more expensive it can be to correct them. In systems engineering practice, there are many methods and tools to reduce the likelihood of systematic faults. In this paper, we present the application of a formal model–based verification technique – called model checking – to assist railway engineers in designing and verifying the safety-related functionality of railway control systems. The proposed process is part of a specification-verification environment that facilitates the construction of correct, complete, consistent, and verifiable functional specifications during development. The results and experience in model checking are illustrated by a case study of a vehicle detection point, a common component in this domain. The model checking of the case study has been performed in the widely used UPPAAL modeling and simulation framework, which can also verify formal properties and generate a counterexample in case of a property violation. By analyzing the counterexample, the designer can gain insights into the system's behavior and identify potential design flaws or failures. Model checking can be used to achieve a higher quality functional specification that is typically more complete and/or contains fewer faults compared to the traditional development approach.

Keywords:

verification, model checking, computation tree logic, railway control system

Citation data from Crossref and Scopus

Published Online

2024-06-04

How to Cite

Lukács, G., Bartha, T. (2024) “Verification of Railway Control Systems Using Model Checking and CTL, Explained Through a Case Study”, Periodica Polytechnica Transportation Engineering, 52(4), pp. 402–411. https://doi.org/10.3311/PPtr.23344

Issue

Section

Articles