高速铁路CTC分界口临时限速系统建模与验证

• 作者: 王长林 赵荣亮
• 来源期刊: 铁路计算机应用
• 学科: 交通运输
• 关键词: 临时限速 CTC分界口 信息交互 实时性 时间自动机 UPPAAL
• 年，卷（期）: 2014,（7）
• 所属期刊栏目: 计算机与通信信号
• 页码范围: 43-47
• 页数: 5页
• 分类号: U284.482|TP39
• 字数: 3324字
• 语种: 中文

摘要

临时限速是高速铁路列控系统的重要组部分,CTC行车调度台分界口处的临时限迷信息交互频繁,对实时性的要求也更苛刻.为满足其实时性要求,采用时间自动机理论,结合分界口处临时限速相邻设备间的交互过程,分别建立各设备的时间自动机模型,通过时间自动机的积构建整个交互系统的网络模型,并利用UPPAAL验证工具对模型的功能和性能属性进行形式化验证.验证结果确认了交互过程中系统的安全性和受限活性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王长林	西南交通大学信息科学与技术学院	67	573	13.0	20.0
2	赵荣亮	西南交通大学信息科学与技术学院	1	6	1.0	1.0