Modeling And Verification Of On-Board Equipment Of CTCS-3 Train Operation Control System Based On Timed Automata

AS the railway system requires high safety all the time, Chinese Train Control System Level 3(CTCS-3)equipment as the high-speed train control system should be more stable and safe. Onboard equipment system is an important component of CTCS-3. UPPAAL is a modeling, analyzing and verifying tool for real-time system based on Timed Automata Theory. It is possible to verify some properties of onboard equipment system by using UPPAAL to model, analyze and verify Vital Computer (VC), Radio Block Center (RBC) and Driver Machine Interface (DMI) of onboard equipment of Automatic Train Control for CTCS-3, and it is significant for guaranteeing the safety of working procedures. Researching onboard equipment modeling, it has important practical of significance for perfect the onboard equipment simulation system performance, speeding up onboard equipment software design, saving the cost of testing.The major works of this thesis are summarized as following:1. This thesis reviews research of modeling Automatic Train Control based on Formal Methods and Timed Automata at home and abroad.2. This thesis introduces the train control onboard equipment structure, functionality and operation modes for CTCS-3.3. This thesis analyses the work in the case of CTCS-3 working procedures, Including start-up of onboard mission procedure, onboard overriding procedure, train trip procedure, procedure triggered by shunting drivers, and end of onboard mission procedure, establishes the state transition diagram of various working procedures, and illustrates the information exchange and the state transition process of onboard equipment.4. This thesis introduces Timed Automata Theory and the method of using this model-test tool UPPAAL.5. The models of VC, DMI and RBC based on Timed Automata Theory are established. After reasonable abstract and assumption, the states of each process, states transition path, states transition constraints and trigger event are determined on Timed Automata Theory, so as to obtain various timed automata models of onboard equipment.6. UPPAAL is used to analyze and verify these timed automata models of onboard equipment system. By using Simulator, the experiments through the channel between the various entries of onboard equipment communicate each other and the control message sequence are obtained, onboard equipment work flow timing diagram is simulated, and analyzing the state transition of model of onboard equipment. By using Verifier, via quickly searching the whole state space of onboard system, accessibility, time characteristics, safety, activity and other properties of onboard equipment are verified.