Modeling And Verification Of RBC Control Train Scene Based On Timed Automata

CTCS-3 Train Control System is the main technical equipment in railway signal field,which is responsible for directing the train operation, ensuring the safety of traffic and improving the efficiency of transportation.The RBC (Raid Block Center) system is the core equipment of the CTCS-3 Train Control System, which is the key to the realization of safe and efficient vehicle control.As the RBC system (safety critical system) not only has the complex function , but also it’s real-time requirements are very high, so the design requirements of RBC system is highly accurate and reliable.However, the traditional system design methods can not find the defects of software errors and hidden dangers in time.In this paper, a formal method based on timed automata theory is used to design and verify the security of RBC system software in order to improve the security, reliability and correctness of RBC system.The essence of formal modeling and verification of RBC system is to find a time automata model research system which is closely related to the prototype.In this paper, based on the analysis of the existing RBC formal modeling technology and its advantages and disadvantages, the formal modeling and verification method of RBC system based on the specification and timed automata theory is studied.Because the RBC is a large system and has complex function as real-time system, in order to describe the system more clearly, take the Standard Specification for CTCS-3 Train Control System as basis, the main train operation scene of RBC system control as the breakthrough point,analyze the control flow of the RBC system in each scene, time automaton model of main function was established, and through the channel and the global variable group, the time automaton network model was built.Then in the UPPAAL tool, the model is simulated. the key function of the system is extracted, and turned it into the BNF syntax statement, in the UPPAAL validator, the validity of network model was verified. The results show that the formal model based on timed automaton theory and RBC specification is feasible, it provides a new way to design a correct and reliable RBC system, which has practical significance in engineering application.