Modeling And Analysis Of RBC System Train-Control Process Based On UPPAAL

RBC system is an important component of Chinese Train Control System Lecel 3 (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 RBC system train-control process of RBC by using UPPAAL, and it is significant for guaranteeing the safety of train-control process.The major works of this thesis are summarized as following:1. This thesis introduces Timed Automata Theory and the method of using this model-test tool UPPAAL.2. By analyzing train control process, there are 5 parts of train-control process: train login process, normal control process, RBC handover process, train logout process and message resend process. Based on these 5 processes, RBC can control a train.3. The models of these 5 processes and other external equipment based on Timed Automata Theory are established. After reasonable abstract and assumption, the states of each process, states transition path and constraints are determined based on Timed Automata Theory, so as to obtain the timed automata model of the 5 process.4. 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 quickly searching the whole state space of RBC system, activity, validity and ohter properties of RBC train control process are verified.