Modeling and verification of high-speed railway train control temporary speed limit switching scenarios based on UML and UPPAAL
ZHOU Xiang
Abstract：To improve the timeliness and safety of the information transmission process in the cross-border overlapping area between the temporary speed restriction server(TSRS)and the radio block center(RBC)for high-speed rail train control temporary speed restriction commands,a mathematical model of the TSRS switch and RBC switch cross-border overlapping area speed restriction process is established.Based on the characteristics of temporary speed restriction command interaction between the Chinese Train Control System(CTCS)CTCS-2/CTCS-3 high-speed rail train control systems,a combined approach of unified modeling language(UML)and Timed Automata model theory is adopted.The formal verification tool UPPAAL is used to identify deficiencies and vulnerabilities in the information transmission of temporary speed restriction commands in the cross-border overlapping area.The research results indicate that train control temporary speed restriction is an important component for the safe operation of high-speed rail.There is frequent information interaction between temporary speed restriction,centralized traffic control(CTC),RBC,train control center(TCC),and other related subsystems.The information transmission processes between different subsystems vary.The verification results of the Timer,Resend,TSRS,and RBC Timed Automata mathematical models show that the transmission time of TSRS switch and RBC switch information in the cross-border overlapping area is less than 3 s,and the information channel of the Timed Automata model does not lead to deadlock situations,significantly improving the timeliness and safety of high-speed rail train operation.
Keywords：temporary speed limittimed automataUMLUPPAALhigh-speed railway train control
Publication Date：2024-09-30
Online Publishing Date：2026-05-22(First online date of this platform, not the publication date of the document)
Pages：8( 31-38 )