Formal Modeling And Analysis Of RBC System Based On UML And TA

RBC(Radio Block Center) is the key equipment of CTCS-3 Train Control System to ensure safe and reliable operation of the train. The safe operation of trains on the line contributes to the information received from the ground equipment and MA(movement authority) formed by GSM-R network and vehicle mounted system for continuous two-way information interaction. RBC highly requires real time. Whether to meet the requirement or not directly affects CTCS-3 system to control train safely, reliably, efficiently and accurately. To ensure the reliable work and real-time requirements of the RBC system, the requirements specification and design specification which guide the design of the train control system must be ensured absolutely right. Otherwise, the risk of potential failure may be turned into a failure of the system, resulting in the occurrence of safety accidents. Therefore, to regulate the modeling and verification of the corresponding will become effective means to ensure the correct and reasonable.The CTCS-3 Train Control System requirements specification regarded as the background, combining the semi formal method for UML(Unified Modeling Language) with formal methods timed automata, the thesis attempts to test the two operation scenes of rating transitions and RBC handover so as to ensure real-time and safety for RBC train control. Firstly, the thesis analyzes the two scenes about system requirement specification and design scheme of the CTCS-3 train as well as divides the all scenes into several moules according to time features. Secondly, according to the requirements of the real-time and dynamic information interaction, each sub module is used for modeling the sequence diagram and timing diagram of UML expansion the characteristics of the time. Thirdly, the UML sequence diagram and timing diagram transformation model for time difference automatic machine model are established on the basis of convert rules from the UML sequence diagram to time automaton. Finally, based on the principle of time automatic machine, the thesis merges all independent time automatic machines into systematic time automaton network model. Besides, applying simulation of the existing model of state transition graph with UPPAAL verification tools, using BNF to verify the statements extracted from the specification, it verifies the real-time and safety properties of the system network model of the whole network one by one so as to ultimately test the verification of standard modeling.The combination, between UML and timed automata in the modeling and verification of the system specification, not only can accurately express the regular semantics, but reasonly verif the performance of the system, which provides referencefor to the perfection of CTCS-3 Train Control System and the study and development to more advanced column control system.