Formal Modeling And Verification Of CBTC Zone Controller Based On Time Automation

With the gradually accelerating pace of urbanization, communication based train control(CBTC) system has became the development trend of city rail transit train control system in the present world. As the core equipment of CBTC system, zone controller(ZC) is the key to realize the safe train tracking, its reliability is directly related to the safety of train operation. In order to discover system design difficience timely and accurately, it is particularly important to use a tool to describe and verify system in the early stage of development. Formal method is a kind of technology based on precise mathematical language to analyze and verify system. The thesis adopts formal method to model and verify ZC aiming to guarantee the correctness and security of ZC design.Firstly, the thesis analyzes the formal methods of current mainstream, then according to the design requirements of safety critical system, a formal method of timed automation and its verification tool UPPAAL are proposed.Secondly, on the basis of analyzing the basic structure and operation principle of CBTC, the working principle of ZC is analyzed thoroughly, then the function and performance requirement of the system is proposed. Due to ZC is a complex real-time system, the function is divided into four modules: train management, movement authority and ZC handover, information interaction beween ZC and other CBTC subsystem. Then flow are designed respectively. According to the flow of train operation in the CBTC region, the functions of ZC are established based on timed antomation by setting the channel and sharing variables realized the communication of several timed automata models, and achieved a complete network of timed automata model.Finally, the message sequence chart is obtained by simulating the model with UPPAAL. This thesis also analyses the change of state of train operation process and communication between subsystems in the CBTC region. Then functions and performance requirements of the system are extracted by using BNF grammer, and successfully verified. Results of the verification show that the formal method of timed automatation is feasible to analyze and verify real-time system, and can provide reference for CBTC to futher study.