应答器报文编制规则的形式化建模与验证

Formal Modeling and Verification of Compilation Rules of Balise Telegram

应答器报文的正确与否直接关系到列车运行安全。CTCS-2级列控系统应答器的应用原则是C2应答器报文编制的起点和依据,应答器报文的正确性与应用原则的正确性及其是否被正确执行直接相关。基于文本语言描述的应答器应用原则易产生二义性问题,存在较大隐患。通过深度挖掘应答器应用原则,并结合列控数据,从中提取出具体报文编制规则,采用UML与NuSMV相结合的方法对具体的编制规则进行形式化建模与验证,并以一种类型的报文生成为例,构建规则的UML模型,对UML模型进行扩展和抽象,将其转换为NuSMV模型,用模型检验工具验证其活性、转移性和确定性等,可以得到应答器应用原则中存在的问题,对确保应答器报文的正确性有重要意义。

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.