基于UML与UPPAAL的高铁列控临时限速切换场景建模与验证

周翔

滨州市交通运输局，山东 滨州  256600

摘要：为提高高速铁路列控临时限速命令在临时限速服务器（temporary speed restriction server，TSRS）与无线闭塞中心（radio block center, RBC）跨界重叠区域信息传递过程的时效性和安全性，建立TSRS切换与RBC切换跨界重叠区域限速流程的数学模型，根据中国列车运行控制系统（Chinese train control system，CTCS）CTCS-2/CTCS-3高铁列控系统间临时限速命令交互的特点，采用统一建模语言（unified modeling language，UML）与时间自动机模型理论相结合的方法，采用形式化验证工具UPPAAL寻找临时限速命令在跨界重叠区域信息传递的不足和漏洞。研究结果表明：列控临时限速是高铁安全运行的重要组成部分，其与高铁列控高铁调度集中（centralized traffic control，CTC）、RBC、列控中心(train control center，TCC)等相关子系统有频繁的信息交互，不同子系统间信息传递过程不同，Timer（时间控制器）、Resend（重发控制器）、TSRS和RBC时间自动机数学模型验证结果为TSRS切换与RBC切换信息在跨界重叠区域的传递时间小于3 s，且时间自动机模型信息通道无锁死情况，大大提高高铁列车运行的时效性和安全性。

关键词：临时限速；时间自动机；UML；UPPAAL；高铁列控

Modeling and verification of high-speed railway train control temporary speed limit switching scenarios based on UML and UPPAAL

ZHOU Xiang

Binzhou Jiaotong Bureau, Binzhou 256600, China

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 limit; timed automata; UML; UPPAAL; high-speed railway train control