Modeling and Verification of Radio Block Center of CTCS-3 Train Control System for Dedicated Passengers Lines
Hao Jia · Journal of the China Railway Society · 2010
This paper analyzes the function and performance of the software of RBC subsystem of CTCS-3 for dedicated passenger railway lines,gives a semiotic semantic description of the RBC subsystem based on the theory of the timed automaton(TA),sets up the TER-QSR timed automaton network model and conducts si-mulation of the RBC subsystem with the UPPAAL verification tool to verify,the safety and bounded liveness of RBC and optimize the handover time of RBC.