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

被引:0
作者
Lukács, Gábor [1 ]
Bartha, Tamás [1 ,2 ]
机构
[1] 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., Budapest
[2] Institute for Computer Science and Control (SZTAKI), Kende street 13-17., Budapest
来源
Periodica Polytechnica Transportation Engineering | 2024年 / 52卷 / 04期
关键词
computation tree logic; model checking; railway control system; verification;
D O I
10.3311/PPtr.23344
中图分类号
学科分类号
摘要
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. © 2024 Budapest University of Technology and Economics. All rights reserved.
引用
收藏
页码:402 / 411
页数:9
相关论文
共 23 条
[1]  
Alshalalfah A.-L., Mohamed O. A., Ouchani S., A framework for modeling and analyzing cyber-physical systems using statistical model checking, Internet of Things, 22, (2023)
[2]  
Arcile J., Devillers R., Klaudel H., VERIFCAR: a framework for modeling and model checking communicating autonomous vehicles, Autonomous Agents and Multi-Agent Systems, 33, pp. 353-381, (2019)
[3]  
Baier C., Katoen J.-P., Principles of model checking, (2008)
[4]  
Bensalem S., Bozga M., Sifakis J., Nguyen T.-H., Compositional verification for component-based systems and application, International Symposium on Automated Technology for Verification and Analysis, (2008)
[5]  
EN 50128 Railway applications – communication, signalling and processing systems – software for railway control protection systems, (2011)
[6]  
EN 50129 Railway applications – communication, signaling and processing systems – safety related electronic systems for signaling, (2018)
[7]  
EN 50126-1 Railway applications – the specification and demonstration of reliability, availability, maintainability and safety (rams) – part 1: generic RAMS process, (2017)
[8]  
EN 50126-2 Railway applications – the specification and demonstration of reliability, availability, maintainability and safety (rams) – part 2: systems approach to safety, (2017)
[9]  
Chatterjee K., Doyen L., Computation tree logic for synchronization properties, International Colloquium on Automata, Languages, and Programing (ICALP 2016), (2016)
[10]  
Cimatti A., Clarke E., Giunchiglia E., Giunchiglia F., Pistore M., Roveri M., Sebastiani R., Tacchella A., NuSMV 2: an OpenSource tool for symbolic model checking, International Conference on Computer Aided Verification, pp. 359-364, (2002)