Application Of EVENT-B Method In Formal Modeling And Verification Of Railway Station Interlocking Specification

Safety-critical system refers to a system that has special requirements for safety and reliability. Railway interlocking system is a typical safety-critical system. Its role is to organize trains and shunting traffic in the railway station, at the same time ensuring its driving safety and driving efficiency. Therefore, it is necessary to use an effective way to ensure its security and reliability as much as possible. Formal description can improve the system design requirements and improve the reliability of the sy'stem development process.This paper takes the interlocking system of railway station as the research object, and analyzes the control flow o f the route selecting, route locking, signal at clear, signal keeping and the route release, and extract some of the more critical environmental specifications and technical specifications. At the same time, this paper establishes the formalization model of interlocking system with Rodin formal modeling and verification tool based on the EVENT-B language. Its corresponding 686 proof obligations have also been proved, and the visualization simulation results show that there is no obvious error. In this process, the function of the interlocking system is described in a more comprehensive way. Finally, the model is instantiated by a typical three-track railway station, and did a further verification and visualization simulation.In this paper, the abstraction description of most functions of the interlocking system is realized. The 686 proof obligations are all certified to be correct, the result of visualization simulation shows that there is no obvious function bug. This shows that EVENT-B language is suitable for formal description to complicated system of railway station interlocking system. The idea of formal description to railway station interlocking system is correct. In addition, the paper puts a solution method to the case that the AXIOM logic is too complex to execution in ProB, and verifies the AXIOM correctness and model consistency. This paper is useful to improve the reliability of the development process of the interlocking system.