Modeling And Semi-physical Simulation Of Train Control Center Based On Timed Automata

With the fast development of Chinese railway system,high-speed train technology has entered a new era.Train Control Center(TCC)is the key ground equipment in Chinese Train Control System level 2(CTCS-2),as well as indispensible backup ground equipment in CTCS-3.It generates and distributes control information to the trains according to track circuit states,messages sent from Computer Based Interlocking(CBI)system as well as Temporary Speed Restriction Server(TSRS),thus ensures the safety of all trains in its jurisdiction.Therefore,the reliability and real-time property of TCC software is crucial to the entire system.To design logical and reliable TCC software,so that it collaboratively takes service in the "High-speed Railway CTCS-3 Virtual Simulation Experiment System" under the laboratory environment,this paper completed the following missions:Firstly,this paper introduced the TCC system in CTCS-2,its functions,components and interfaces with other subsystems so as to lay a solid base for the modeling and design of TCC soft,Aware.Secondly,a comparison was made between different formal methods.The article illustrates the reason why Timed Automaton theory was chosen as the modelling principle based on the characteristic of TCC software,and briefly introduces the definition^ semantics and syntax of Timed Automaton.Last but not least,it gave a sketch of the V&V tool UPPAAL applied on Timed Automaton theory.Thirdly,the design and verification of a hierarchical model was laid.This paper analyzed the procedure of track circuit low frequency encodement and controlled-data balise telegram encodement based on function requirements.On account of previous research,it chose the encoding process of controlled-data balise telegram as an example to build a hierarchical model based on scenarios.A 6-layer model was put forward and the automata network was formed by channels and global variables.The validity and performance of this proposed model was checked via the simulator and verifier of UPPAAL.The result showed this model illustrates the TCC interface with other systems more clearly and reduced subjective factors compared with the previous model.Finally,this paper implemented the designed model into TCC software using C#and MySQL,based on the technical manual on TCC of passenger dedicated lines.This TCC software can encode the controlled-data balise telegrams as well as track circuit’s low frequencies according the dispatching commands,route states,line parameters and location of trains.The designed TCC software can work properly and meet the demands of the CTCS-3 simulation system.