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

摘要：

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

关键词：应答器报文、应答器应用原则、符号模型检验、UML

所属期刊栏目：41

分类号：U284(铁路通信、信号)

资助基金：中央高校基本科研业务费2017JBM009

在线出版日期：2019-08-09（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：100-106