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

打开文本图片集

摘要：为提高高速铁路列控临时限速命令在临时限速服务器（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寻找临时限速命令在跨界重叠区域信息传递的不足和漏洞。（剩余11731字）