Formal Method for Behavior Verification and Data Validation of Station Interlocking System
-
摘要: 车站联锁系统是一种典型的基于数据驱动的安全苛求系统，开发过程中需要对系统行为进行验证并需确认数据的正确性. 为此，通过分析联锁系统的设计规范，基于RODIN平台并使用Event-B语言，辅助使用UML （unified modeling language）图工具快速建立系统的初始模型，以自动生成模型文件并描述出各系统属性与事件流程；基于精化策略分层建模，对各层模型的证明义务进行定理证明，验证了系统的各项属性，得出可靠的通用功能模型；基于实例车站，对模型的公理进行了验证，同时实现了对联锁数据的确认；通过形式化验证过程，结合给定场景联锁数据的有效性确认，发现并纠正系统需求及分析过程中造成的潜在行为缺陷；通过功能仿真与验收测试，进一步确认了通用模型与联锁数据的正确性. 结果表明：本文方法提高了基于模型开发过程的准确性与层次性，验证了系统通用行为状态，且结合公理验证，实现了联锁数据的确认，并能基于模型进行功能场景仿真与测试，从而可进一步提高系统通用功能原型的可靠性.Abstract: Station interlocking system is a typical safety-critical system driven by data, which needs to verify the system behavior and confirm the correctness of data in the development. After analyzing the design specifications of the interlocking system, the initial system model was built automatically by the UML (unified modeling language) diagram, with the system properties and event flows described by Event-B language on RODIN platform. Subsequently, the refinement policy was used for hierarchical modeling, and the proof obligations of each layer were proved by theorem and the properties of the system attributions were verified. Thus, a reliable universal function model was obtained. Using a real station yard, the axioms of the model were proved and the interlocking data were validated as well. According to the formal verification and data validation in a given scenario, the subtle defects generated in the analysis of the system requirements could be found and corrected. Finally, the functional simulation and acceptance testing confirmed the correctness of the general model and the interlock data. This method not only improves the accuracy and hierarchy of the model-based development, but also verifies the universal behavior state of the system. Combined with axiomatic verification, the validation of interlocking data is realized. The function scenario can be simulated and tested based on the model, which can further improve the reliability of the universal function prototype of the system.
-
Key words:
- station interlocking system /
- formal verification /
- theorem proving /
- data validation /
- functional simulation /
- testing
-
表 1 模型各层精化内容
Table 1. Refinement of the model
精化层级 引入对象 第 1 层 建立列车对象，构造进路相关事件基本功能流程，如建立进路、进路正常解锁、进路取消、进路人工延时解锁和进路故障解锁等 第 2 层 建立进路类型、进路方向、轨道区段类型、列车类型和敌对进路的定义，描述与进路、轨道区段、列车相关的功能与安全属性 第 3 层 建立道岔对象，将道岔锁闭和解锁流程同步在建立进路和解锁进路事件中 第 4 层 添加道岔的位置信息，增加道岔转动的计时约束，完善与道岔相关的事件 第 5 层 建立信号机对象，完善人工延时解锁、取消进路等事件 第 6 层 定义进路进程，增加信号设备故障和修复等事件，完善故障解锁流程 
下载: 导出CSV
表 2 模型证明义务的证明情况统计
Table 2. Proving statistics of model proof obligations
条 文件名称 总数 自动 手动 已修正 未通过 C0 1 1 0 0 0 C1 6 5 1 0 0 C2 4 2 2 0 0 C3 2 2 0 0 0 C4 6 6 0 0 0 C5 5 3 2 0 0 C6 0 0 0 0 0 M0 0 0 0 0 0 M1 80 49 31 0 0 M2 59 17 42 0 0 M3 46 17 29 0 0 M4 118 41 77 0 0 M5 146 61 85 0 0 M6 237 218 19 0 0 总计 710 422 288 0 0
下载: 导出CSV
表 3 举例车站联锁表
Table 3. Interlocking table of the example station
方向 进路 信号机 道岔 轨道区段 出站轨道区段 敌对信号 敌对进路 迎面敌对 进路编号 名称 显示 发车进路 股道 Ⅰ至 X SⅠ L 1、3 1/3DG Q_1 X 1 — 7 股道 Ⅱ至 X SⅡ L 1、（3） 1/3DG Q_1 X 2 — 8 股道 Ⅲ至 X SⅢ L （1）、{3} 1/3DG Q_1 X 3 — 9 股道 Ⅰ至 S XⅠ L 2、4 2/4DG Q_2 S 4 — 10 股道 Ⅱ至 S XⅡ L （2）、{4} 2/4DG Q_2 S 5 — 11 股道 Ⅲ至 S XⅢ L 2、（4） 2/4DG Q_2 S 6 — 12 注：信号机中，L表示绿灯；道岔中，1表示1# 道岔在定位，（1）表示1# 道岔在反位，{1}表示1# 道岔带动在定位，其余类推；轨道区段中，1/3DG表示1～3轨道区段，2/4DG表示2～4轨道区段.
下载: 导出CSV
表 4 公理验证结果
Table 4. Verification of axioms
条 文件名称 总数 自动 手动 已修正 未通过 C0 7 3 4 0 0 C1 22 7 14 0 1 C1_1 6 3 3 0 0 C2 15 2 13 0 0 C3 9 3 6 0 0 C4 20 16 4 0 0 C5 14 0 14 0 0 C6 0 0 0 0 0 总计 93 34 58 0 1
下载: 导出CSV
-
王恪铭,王峥. 基于形式化方法的道口控制系统规范建模与验证[J]. 西南交通大学学报,2019,54(3): 573-578,603.WANG Keming, WANG Zheng. Modeling and verification of control system specification for railway level crossings based on formal method[J]. Journal of Southwest Jiaotong University, 2019, 54(3): 573-578,603. International Electrotechnical Commision. Functional safety of electrical/electronic/programmable electronic safety-reared systems: IEC 61508[S]. Geneva: European Committee for Electrotechnical Standardization. 2005. KHAN U, AHMAD J, SAEED T, et al. On the real time modeling of interlocking system of passenger lines of Rawalpindi Cantt train station[J]. Complex Adaptive Systems Modeling, 2016, 4(1): 1-33. doi: 10.1186/s40294-016-0028-5 VU L H, HAXTHAUSEN A E, PELESKA J. Formal modelling and verification of interlocking systems featuring sequential release[J]. Science of Computer Programming, 2017, 133: 91-115. doi: 10.1016/j.scico.2016.05.010 BONACCHI A, FANTECHI A, BACHERINI S, et al. Validation process for railway interlocking systems[J]. Science of Computer Programming., 2016, 128: 2-21. doi: 10.1016/j.scico.2016.04.004 HANSEN D, SCHNEIDER D, LEUSCHEL M. Using B and ProB for data validation projects[C]//Inernational Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. [S.l.]: Springer, 2016: 167-182. ABRIAL J R. Train system[M]//Modeling in Event-B. Cambridge: Cambridge University Press, 2013: 508-549. 国家铁路局. 铁路车站计算机联锁技术条件: TB/T 3027—2015[S]. 北京: 中国铁道出版社. 2015. 张传东. EVENT-B方法在铁路车站联锁规范形式化建模与验证中的应用研究[D]. 成都: 西南交通大学, 2017. ZHANG Chuandong, WANG Keming, WANG Xia, et al. Interlocking data[DB/OL]. [2019-08-16]. https://github.com/abidefei/Model_Verification_Data_Validation_Interlocking_EventB. SNOOK C, HOANG T S, DGHYAM D, et al. Behaviour-driven formal model development[M]//Formal Methods and Software Engineering. Cham: Springer International Publishing, 2018: 21-36. -
下载:
点击查看大图
图(7) / 表(4)
计量
- 文章访问数: 437
- HTML全文浏览量: 206
- PDF下载量: 28
- 被引次数: 0