Formal Modeling and Verification of the Functionality of Electronic Urban Railway Control Systems Through a Case Study

Urban Rail Transit

Original Research Papers

Gábor Lukács¹  Tamás Bartha² 

[1] Department of Control for Transportation and Vehicle Systems, Budapest University of Technology and Economics, Budapest, Hungary;Department of Control for Transportation and Vehicle Systems, Budapest University of Technology and Economics, Budapest, Hungary;Systems and Control Laboratory, Institute for Computer Science and Control (SZTAKI), Budapest, Hungary;

关键词: Requirement specifications;    Statechart;    Model checking;    Safety critical;    Urban railway control;   

DOI  :  10.1007/s40864-022-00177-8

 received in 2021-10-04, accepted in 2022-09-16,  发布年份 2022

来源: Springer

【 摘 要 】

This paper presents a formal model-based methodology to support railway engineers in the design of safe electronic urban railway control systems. The purpose of our research is to overcome the deficiencies of existing traditional design methodologies, namely the incompleteness and the potential presence of contradictions in the system specification resulting from non-formal development techniques. We illustrate the application of the methodology via a case study of a tram-road level crossing protection system. It was chosen partly because it has a simple architecture and a small number of elements, thus it fits the scope limitations of this article. At the same time, it is suitable for presenting all essential features of our methodology. The proposed solution provides a specification/verification environment that facilitates the construction of correct, complete, consistent, and verifiable functional specifications during the development, while hiding all the formal method-related details from the railway engineers writing the specifications. Using this formal model-based methodology, a high-quality functional specification can be achieved, which is guaranteed to be more exhaustive and will contain fewer errors than traditional development.

【 授权许可】

CC BY   
© The Author(s) 2022

【 图 表 】

Fig. 2

Fig. 4

Fig. 5

Fig. 3

12888_2022_4137_Article_IEq2.gif

Fig. 6

Fig. 2

Fig. 7

13068_2022_2229_Article_IEq3.gif

13068_2022_2229_Article_IEq2.gif

Fig. 1

Fig. 4

12951_2022_1749_Article_IEq8.gif

Fig. 5

Fig. 6

Fig. 5

Fig. 4

12864_2022_9026_Article_IEq187.gif

Fig. 7

12888_2022_4322_Article_IEq11.gif

12888_2022_4322_Article_IEq5.gif

Fig. 1

12936_2022_4393_Article_IEq6.gif

Fig. 13

12888_2022_4322_Article_IEq1.gif

Fig. 3

Fig. 6

Fig. 1