Formal Modeling And Verification Of Automatic Train Protection System

Automatic train protection (ATP) system is the core of the train control system, the safety and reliability of the system is directly related to the safe operation of trains. ATP system is a safety critical real-time system. The function of system is complicated and communicate with each other frequently. There is a higher demand for real-time, not only the computation result is correct in logic, but also the result satisfy the time constraints of certain. How to ensure the ATP system function is consist with the requirement specification and guarantee the correctness and security of system function need to be solved by researchers.Formal method is based on the strict mathematics theory as the foundation, can accurately describe the specification requirement system and avoid the natural language arbitrariness to solve the problem. Based on the formal method’s analysis and comparison, choose timed automata theory to describe real-time concurrent system function process. Timed automata theory is introduced in detail by ATP system and the method of constructing the system of timed automata network model is studied. And the model verification tool UPPAAL are studied in detail.Automatic train protection system is the research object, analysis the structure and function of the system, and focus on the speed supervision and protection function and the synchronization function. According to the functional requirements of the system, we adopt UPPAAL to model the ATP’s function process, and verify the security and liveness of the system. The consistency of model function and the demand of the system is proved. Formal method is the important way to guarantee the validity and safety of ATP system function process. We use VC6.0software tool to design ATP vehicle speed protection model, the simulation system can achieve the speed monitoring and protection function.