Modeling Analysis And Verification Of Zone Controller In Communication Based Train Control System

With the rapid development of urban rail transit construction in major cities,the Communication Based Train Control(CBTC)system has become the main development direction of urban rail transit because of its high reliability and high security.People put forward higher requirements for the high speed and high safety of train operations.Zone Controller(ZC),is a key part of the CBTC system to ensure the safe operation of the train,bears a major responsibility for the safe travel of citizens.ZC is a system with a complex internal structure and real-time,any possible design flaws in its internal function modules may cause irreparable consequences.In order to find out the possible defects in the system more timely and accurately,taking advantage of formal methods to describe the system architecture and functions as rigorously and accurately as possible and verifying the requirements is of great significance for ensuring the safety of urban rail transportation in the early stages of the deep development of the system.ZC is selected as the major research object in the thesis.The ZC boundary switching module and train tracking module are described by the time automaton theory,and the requirements of functionality and real-time of ZC sub-system are verified by the UPPAAL verification tool.First of all,the basic structure of CBTC,the functional structure of ZC,and the information interaction process among subsystems in CBTC are introduced in the thesis.The scenes of train crossing the ZC boundary and the train tracking are carried out,and the actual conditions of the process of ZC boundary switching and the specific process of train tracking are analyzed in depth,which lays a theoretical foundation for modeling and verification of ZC under the two scenes.Secondly,through analyzing the specific operation of different positions in the process of train crossing the ZC boundary,combining the information interaction relationship between the train and the two regional controllers,a time automaton network model of ZC boundary switching is established using the time automata theory.Through analyzing the specific processing of train tracking,combining with the information flow between the modules within the ZC during the process of train tracking,time automaton network model of the train sieving,the train tracking demarcation point and two trains tracking in the same section is established by the time automata theory.Finally,the functional requirements and performance of ZC under the ZC boundary switching scene and train tracking scene are compiled by Backus Normal Form(BNF).The formal BNF grammar is verified in the UPPAAL verify window,and the verification of the functionality and real-time performance of the system in two scenes is realized.The theoretical reference is provided for optimizing the performance and deep development of ZC in the early stage of design and development.