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

• 作者: 刘中田 黄旭
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: 应答器报文 应答器应用原则 符号模型检验 UML
• 年，卷（期）: 2019,（6）
• 所属期刊栏目: 铁道通信信号、信息化
• 页码范围: 100-106
• 页数: 7页
• 分类号: U284
• 字数: 6607字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2019.06.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘中田	北京交通大学电子信息工程学院	24	145	7.0	10.0
2	黄旭		1	0	0.0	0.0