基于UPPAAL的高铁列控系统等级转换过程建模与验证

• 作者: 吕继东 康仁伟 王俊峰
• 来源期刊: 北京交通大学学报
• 学科: 交通运输
• 关键词: CTCS-2/CTCS-3等级转换 时间自动机 UPPAAL 安全性
• 年，卷（期）: 2012,（6）
• 所属期刊栏目: 铁路运输工程与道路工程
• 页码范围: 63-67,73
• 页数: 6页
• 分类号: U283.4
• 字数: 4600字
• 语种: 中文

摘要

为了满足铁路线路互联互通以及设备故障之后列车降级运行的需求,列车在运行过程中需要进行等级转换.等级转换过程中,车载设备未正常接收转换预告点、转换执行点应答器的信息,或者列车速度未降至线路允许速度以下等因素,可能导致等级转换不成功,因此有必要通过形式化建模对转换过程分析和验证.本文提出了一种基于UPPAAL的等级转换过程建模与验证方法.采用时间自动机理论建立了CTCS-2/CTCS-3等级转换过程的时间自动机网络模型,应用UPPAAL验证工具对等级转换过程进行仿真分析,验证了等级转换过程的安全性,并对现有技术规范提出了改进意见.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王俊峰	北京交通大学轨道交通控制与安全国家重点实验室	30	196	8.0	13.0
2	吕继东	北京交通大学轨道交通运行控制系统国家工程研究中心	25	310	9.0	17.0
3	康仁伟	北京交通大学轨道交通控制与安全国家重点实验室	2	40	2.0	2.0