基于SAT的应答器工程数据逻辑规则提取及验证

Extraction and Verification of Logic Rules of Balise Engineering Data Based on SAT

工程数据是应答器报文编制的重要依据,现有工程数据验证规则是基于CTCS-2级列控系统应答器应用原则及工程数据表编制规范生成的,这类基于文本语言描述的规则完备性不足,且存在二义性,数据验证不充分,易直接导致数据安全问题。因此,本文深度挖掘各类工程数据间的约束关系,提取数据逻辑验证规则,通过基于SAT的形式化建模、ROBDD构造及深度优先搜索来证明逻辑规则的可满足性。开发基于导出逻辑规则的数据验证工具,并以某城际线路工程数据表为例,与传统工程数据表检查软件进行比较。结果表明,新工具能够识别传统软件无法识别的数据隐患,消除传统验证规则的不完备性,提高工程数据的安全性。

Engineering data are the important basis for balise telegram compilation.Existing engineering data verification rules are generated based on balise application principles and engineering data compilation specification of CTCS-2.These rules,described by natural languages,are characterized by lack of completeness,ambiguity and data validation insufficiency,which may directly lead to data safety problems.To address the above issues,data logic verification rules were derived firstly based on the deep data mining of constraint relationship between various kinds of data,to extract data logic verification rules.Then,the satisfiability feature of the logic rules was proved through SAT modeling,ROBDD constructing and depth-first search algorithm.A data verification tool based on the derived logic rules was developed finally.Based on the engineering data sheet of an intercity mass transit line,the engineering data were verified with this tool,as well as another traditional data check software.The results showed that,the new tool can identify data hazards which cannot be found by the traditional software,thus eliminating the incompleteness of primitive verification rules and greatly improving the engineering data safety.