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

第 3 9 卷 第 2 期 铁 道 学 报 Vol. 39 No. 2 2 0 1 7 年 2 月 JO U R N A L OF T H E C H IN A RAILW AY SOCIETY February 2017 文章编号：1001-8360(2017)02-0082-08 基于S A T 的应答器工程数据逻辑规则提取及验证 王彤典U ，赵会兵1 (1 . 北京交通大学电子信息工程学院，北 京 1〇〇〇4 4 ; 2 . 北京交通大学轨道交通控制与安全国家重点实验室，北 京 100044) 摘 要 ：工程数据是应答器报文编制的重要依据，现有工程数据验证规则是基于C T C S -2 级列控系统应答器应 用原则及工程数据表编制规范生成的，这类基于文本语言描述的规则完备性不足，且存在二义性，数据验证不充 分 ，易直接导致数据安全问题。因此，本文深度挖掘各类工程数据间的约束关系，提取数据逻辑验证规则，通过 基 于 S A T 的形式化建模、R OBDD 构造及深度优先搜素来证明逻辑规则的可满足性。开发基于导出逻辑规则的 数据验证工具，并以某城际线路工程数据表为例，与传统工程数据表检查软件进行比较。结果表明，新工具能够 识别传统软件无法识别的数据隐患，消除传统验证规则的不完备性，提高工程数据的安全性。 关键 词 ：应答器；数据安全；逻辑验证规则；SA T; ROBDD 中图分类号：TP302. 1;U 283. 2 文献标志码 ： A doi ：10. 3969/j. issn. 1001-8360. 2017. 02. 012 Extraction and Verification of Logic Rules of Balise Engineering Data Based on SAT WANG Tongdian1，2 , ZHAO Huibing1 (1. School of Electronic and Information. Engineering, Beijing Jiaotong U niversity, Beijing 100044» C hina ； 2. State Key Lab of Rail T raffic Control and Safety, Beijing Jiaotong U niversity, Beijing 100044» China) Abstrac ：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 specifica­ tion of CTCS-2. These rules, described by natural languages, are characterized by lack of completeness, am­ biguity and data validation insufficiency, which may directly lead to data safet