基于形式化方法的道口控制系统规范建模与验证  

Modeling and Verification of Control System Specification for Railway Level Crossings Based on Formal Method

作　　者：王恪铭 王峥[1] WANG Keming;WANG Zheng(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,China;National-LocalJoint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu610031,China)

机构地区：[1]西南交通大学信息科学与技术学院,四川成都611756 [2]西南交通大学系统可信性自动验证国家地方联合工程实验室,四川成都610031

出　　处：《西南交通大学学报》2019年第3期573-578,603,共7页Journal of Southwest Jiaotong University

基　　金：国家自然科学基金资助项目(71502146,61673320);中央高校基本科研业务费资助项目(2682017ZT12)

摘　　要：为了增强铁路道口控制系统设计的可靠性,使用一种形式化方法对该系统进行建模与验证.基于道口管理规范,在分析系统各类属性与事件流程的基础上,使用 UML 图方法并结合精化策略建立了系统各层的 Event-B语言模型.通过对不变式的证明义务进行证明,验证了系统设计中的安全、时间特性,检查出了需求规范分析中的缺陷,提出了增强系统稳健性的改进方案,修正了系统的设计原型.最后,通过不变式冲突与死锁检验进一步确认了模型的正确性.研究表明文中方法提高了形式化建模过程的准确性与层次性,且确认得出目前规范中存在列车驶入道口时不能确保道口出清的缺陷,证实了使用本文形式化流程可以验证道口控制系统的需求规范并形成可靠的设计原型,从而可提高铁路道口的安全性.To improve the reliability of the control system design for the railway level crossings,a formal method is used to model and verify this system. By analyzing the management standards of the railway crossingss,the requirement properties and event processes were obtained;moreover,a multilayer Event-B model was established by using the UML diagram method and refinement policy. After theorem proving of the proof obligations generated by the invariants, the design properties of safety and time were verified;meanwhile the defect of requirement specifications were detected, with an improved event flow being proposed to enhance the robustness,thereof the system prototype was revised as well. Finally,by checking the invariant violations and deadlock,the model was validated on its correctness. The proposed method helps to improve the accuracy and hierarchy of the formal modeling process. In addition,the research result indicates that a defect exists in the current specification, i.e. the clearance of the crossings cannot be guaranteed when the train enters the level crossings. It’s concluded that the formal process presented in this paper can be used to verify the requirement specification of the railway crossings control system,so as to help developing a reliable prototype that can greatly improve the safety of the railway level crossings.

关 键 词：铁路运输 铁路道口 需求规范 形式化方法 系统设计 模型验证 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构] U213.8[自动化与计算机技术—计算机科学与技术]