CTCS-3级列控系统临时限速建模与验证

• 作者: 吕继东 康仁伟 王俊峰 袁磊
• 来源期刊: 西南交通大学学报
• 学科: 交通运输
• 关键词: CTCS-3级列控系统 临时限速 时间自动机 UPPAAL 实时性
• 年，卷（期）: 2013,（4）
• 页码范围: 708-714
• 页数: 7页
• 分类号: U283.4
• 字数: 4201字
• 语种: 中文
• DOI: 10.3969/j.issn.0258-2724.2013.04.018

摘要

为了满足临时限速系统的实时性要求,采用时间自动机理论,对CTCS-3级列控系统临时限速工作流程分别建立了各设备的时间自动机子模型,进而构成临时限速系统的时间自动机网络模型,并基于临时限速系统技术规范的参数对模型进行赋值；采用BNF语法对临时限速系统待验证的属性进行了形式化描述,并应用UPPAAL验证工具对临时限速模型的安全性和受限活性进行仿真验证.验证结果表明:与现有临时限速系统的时间参数设置相比,修正后的时间参数设置避免了出现系统死锁现象；在不影响安全功能属性和受限活性的基础上,提高了临时限速系统的实时性,可在规范规定时间5 s内做出响应.

作者信息

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