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

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