| 应答器报文编制规则的形式化建模与验证 |
| |
| 引用本文： | 黄旭,刘中田. 应答器报文编制规则的形式化建模与验证[J]. 铁道学报, 2019, 0(6): 100-106 |
| |
| 作者姓名： | 黄旭 刘中田 |
| |
| 作者单位： | 中铁第一勘察设计院集团有限公司;北京交通大学电子信息工程学院 |
| |
| 基金项目： | 中央高校基本科研业务费(2017JBM009) |
| |
| 摘 要： | 应答器报文的正确与否直接关系到列车运行安全。CTCS-2级列控系统应答器的应用原则是C2应答器报文编制的起点和依据,应答器报文的正确性与应用原则的正确性及其是否被正确执行直接相关。基于文本语言描述的应答器应用原则易产生二义性问题,存在较大隐患。通过深度挖掘应答器应用原则,并结合列控数据,从中提取出具体报文编制规则,采用UML与NuSMV相结合的方法对具体的编制规则进行形式化建模与验证,并以一种类型的报文生成为例,构建规则的UML模型,对UML模型进行扩展和抽象,将其转换为NuSMV模型,用模型检验工具验证其活性、转移性和确定性等,可以得到应答器应用原则中存在的问题,对确保应答器报文的正确性有重要意义。
|
| 关 键 词： | 应答器报文 应答器应用原则 符号模型检验 UML |
Formal Modeling and Verification of Compilation Rules of Balise Telegram |
| |
| HUANG Xu,LIU Zhongtian. Formal Modeling and Verification of Compilation Rules of Balise Telegram[J]. Journal of the China railway Society, 2019, 0(6): 100-106 |
| |
| Authors: | HUANG Xu LIU Zhongtian |
| |
| Affiliation: | (China Railway First Survey and Design Institute Group Co.,Ltd.,Xi’ an 710043,China;School of Electronic and Information Engineering,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Abstract: | HUANG Xu;LIU Zhongtian(China Railway First Survey and Design Institute Group Co.,Ltd.,Xi’ an 710043,China;School of Electronic and Information Engineering,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Keywords: | balise telegram balise application principle symbolic model checking UML |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
