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.