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

为了增强铁路道口控制系统设计的可靠性，使用一种形式化方法对该系统进行建模与验证. 基于道口管理规范，在分析系统各类属性与事件流程的基础上，使用UML图方法并结合精化策略建立了系统各层的Event-B语言模型. 通过对不变式的证明义务进行证明，验证了系统设计中的安全、时间特性，检查出了需求规范分析中的缺陷，提出了增强系统稳健性的改进方案，修正了系统的设计原型. 最后，通过不变式冲突与死锁检验进一步确认了模型的正确性. 研究表明文中方法提高了形式化建模过程的准确性与层次性，且确认得出目前规范中存在列车驶入道口时不能确保道口出清的缺陷，证实了使用本文形式化流程可以验证道口控制系统的需求规范并形成可靠的设计原型，从而可提高铁路道口的安全性. 

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

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.