Research On RBC Train-Control Process Based On Timed Automata

This thesis researches CTCS-3 level out the ground control subsystem RBC(Radio Block Center),which is a real-time vehicle control system based on wireless communications in the railway signal train control system. Control vehicle functions are the core components in the CTCS-3 level control system. The main content is based on the theory of timed automata. UPPAAL which is the most advanced real-time system modeling and analysis tool ,is used here to verify, model and validate the RBC system. The RBC system is verified finally and has an important practical significance to guarantee the security of control vehicle flow, reduce the system development cycles and development costs.The main content of this thesis includes the exordium, the theory introduction of formal language and timed automata, the requirement analysis of RBC, the molding process of RBC system timed automata and the verification of the functional characteristic with UPPAAL:Chapter1. An overview of the train control system at home and abroad is provided here. The purpose and significance of formal modeling of RBC system is discussed.Chapter2. The advantages and disadvantages of formal language modeling is introduced .and it illustrates the reason for choosing timed automata as the molding tool of RBC.Chapter3. After detailed analysis function requirements of RBC system, it sets up a message resend process. According to the train operation requirement the control flow is divided into four flows:trainlogin process, normal control process, RBC handover process, train logout process .Chapter4. How to use the timed automata model checking tool -UPPAAL is introduced here. RBC system for the five process timed automata model, as well as other external devices timed automata model are established in the UPPAAL.Chapter5. UPPAAL is used to analyse and verify these 5 timed automata models. By setting channel and global variables, the product of timed automata is obtained. By using Simulator, the process of RBC control train is simulated, and analyzing the state transition of RBC train control process is analyzed. By using Verifier, via quiekly searching the whole state space of RBC system, activity, validity and other properties of RBC train control process are verified.