Formal Modeling and Verification of Compilation Rules of Balise Telegram

被引：0
|
作者：
Huang X. [1 ,2 ]
Liu Z. [2 ]
机构：
[1] China Railway First Survey and Design Institute Group Co., Ltd., Xi'an
[2] School of Electronic and Information Engineering, Beijing Jiaotong University, Beijing
来源：
Tiedao Xuebao/Journal of the China Railway Society | 2019年 / 41卷 / 06期
关键词：
Balise application principle; Balise telegram; Symbolic model checking; UML;
D O I：
10.3969/j.issn.1001-8360.2019.06.014
中图分类号：
学科分类号：
摘要：
The correctness of the balise telegram is directly related to the safety of train operation. Balise application principle of CTCS-2 is the starting point and basis of the telegram compilation. The correctness of balise telegram is directly related to the correctness of application principle and whether it can be correctly implemented. The application principle of balise based on text language description may have great hidden problems as it is liable to cause ambiguity. In this paper, the compilation rules of balise telegram were extracted firstly based on the deep excavation of balise application principle and train control data. Then, the method combining UML and symbolic model checking was used to carry out formal modeling and verification of the rules. Finally, based on the balise telegram generation scenario, the UML model of the rules was established, and was expanded and abstracted to transform it into NuSMV model. In the end, the model checking tool was used to verify its activity, transferability and certainty. The results of the analysis of the compilation rules of balise telegram can be used to obtain the problems in the balise application principle, which is of great significance to ensure the correctness of the balise telegram. © 2019, Department of Journal of the China Railway Society. All right reserved.
引用
收藏
页码：100 / 106
页数：6
相关论文
共 10 条
  • [1] ERTMS/ETCS-Class1: FFFIS for Eurobalise. REF: SUBSET-036, V2.2.1, (2003)
  • [2] Wang T., Zhao H., Extraction and Verification of Balise Engineering Data Logic Rules Based on SAT, Journal of the China Railway Society, 39, 2, pp. 82-89, (2017)
  • [3] Zhang Y., Zhao H., Quan H., Et al., Research on Optimization and Fast Coding Method of Balise Telegram, Journal of the China Railway Society, 37, 2, pp. 52-57, (2015)
  • [4] Xiao T., Zhao H., Research on the Safety of Eurobalise Coding, Journal of the China Railway Society, 30, 6, pp. 127-130, (2008)
  • [5] Xing Y., Brief Analysis on the Balise Application Principle of Train Control System, Railway Signalling & Communication Engineering, 9, 5, pp. 1-2, (2012)
  • [6] Liu J., Tang T., Xu T., Et al., Formal Verification of CTCS-3 System Requirements Specification Based UML Model, Journal of the China Railway Science, 32, 3, pp. 93-99, (2011)
  • [7] Quielle J.P., Sifakis J., Specification and Verification of Concurrent Systems in CESAR, Proceedings of the Fifth Intemation Symposium in Programming, (1981)
  • [8] Clarke E.M., Emerson E.A., Design and Synthes is of Synchronization Skeletons Using Branching Time Temporal Logic, Logic of Programs, Workshop, pp. 52-71, (1981)
  • [9] Clarke E.M., Grumberg O., Peled D.A., Model Checking, pp. 193-195, (1999)
  • [10] Kenneth L.M., Symbolic Model Checking, (1993)
1