The Train’s Safety Distance Control Formal Modeling And Verification

Recent years the development of China’s railway very fast, while the train operationsafety issues attracting people’ attention. The core functions of Automatic train protectionsystem(ATP) is to ensure traffic safety of trains, maximize the safety of train operation.Automatic train protection system is core of train control system, the function of trainpositioning is that it can obtain the train’s important information at any time and position thatincluding interval train traffic, speed, acceleration and other important information. Themodern automatic train protection system uses advanced information technology. However,since this system has a systematic, network-based, real-time complexity of the strong mixingproperties and distribution of its characteristics, then its need to use formal methods toestablish the corresponding equipment system model, and it can better understanding andanalysis automatic train protection system, then in the logical correctness, completeness andfunctionality of the overall consistency of the performance to observation system it cost less.Formal modeling and simulation language Event-B develop very fast. Its modeling andsimulation platform provided by the software Rodin. After the part of the language Machinesection through constant refine and using computer simulation which to the behavior of theevent invariant to achieve the effect of system status simulate real effect; After the part of thelanguage Context section continuous extend, simulated environment may tend to be morerealistic environment. At the same time, Event-B has the mathematical theory of generalapplication of formal methods theory. The language calculated by mathematically, andchecking the logical correctness and completeness of the system able to process various statesof system operation were expressed. Therefore, the formal modeling approach for formalmodeling system can play an effective role in the simulation.Its needs a unified and consistent high-level semantic theory to build theorems to ensurethe correct model can be transformed and effective verification, this will ensure thecorrectness of the model generated, and provide tools to support validation of the modelspecification and refinement. Event-B language is strictly based on the mathematicaldefinition of formal methods to accurately and clearly describe the characteristics of thesystem structure. Its studies the problem of safe distance of high-speed trains using formalmodeling and verification method Event-B, and use Rodin as the basic for a formal simulationtools. By combining multi-agent theory, Introducing rules of perception and achieve thecommunication between train and RBC. The simulation research on the minimum interval ofhigh-speed train, and modeling and verification on the trains safety distance control problems.The simulation results show that formal verification methods combined with Event-B andmulti-agent systems can standardized model validation the behavior of complex logic associated with the train control system of CTCS, and for logic verification of complexsystems the method has a strong practical significance.