基于UPPAAL的高铁列控系统等级转换过程建模与验证
康仁伟1
王俊峰1
吕继东2
1.北京交通大学轨道交通控制与安全国家重点实验室,北京,1000442.北京交通大学轨道交通运行控制系统国家工程研究中心,北京,100044
摘要：为了满足铁路线路互联互通以及设备故障之后列车降级运行的需求,列车在运行过程中需要进行等级转换.等级转换过程中,车载设备未正常接收转换预告点、转换执行点应答器的信息,或者列车速度未降至线路允许速度以下等因素,可能导致等级转换不成功,因此有必要通过形式化建模对转换过程分析和验证.本文提出了一种基于UPPAAL的等级转换过程建模与验证方法.采用时间自动机理论建立了CTCS-2/CTCS-3等级转换过程的时间自动机网络模型,应用UPPAAL验证工具对等级转换过程进行仿真分析,验证了等级转换过程的安全性,并对现有技术规范提出了改进意见.
关键词：CTCS-2/CTCS-3等级转换时间自动机UPPAAL安全性
分类号：U283.4(铁路通信、信号)
资助基金：轨道交通控制与安全国家重点实验室自主课题(RCS2011ZZ001)轨道交通控制与安全国家重点实验室开放基金(RCS2011K010)中央高校基本科研业务费专项(2012JBM024,2012JBZ014)
论文发表日期：2012-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：6( 63-67,73 )
英文信息