基于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,且时间自动机模型信息通道无锁死情况,大大提高高铁列车运行的时效性和安全性.
关键词：临时限速时间自动机UMLUPPAAL高铁列控
分类号：U284.48(铁路通信、信号)
论文发表日期：2024-09-30
在线出版日期：2026-05-22（本平台首次上网日期，不代表文献的发表时间）
页数：8( 31-38 )
英文信息