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

被引：14

作者：

袁磊 ^{[1
]}

王俊峰 ^{[1
]}

康仁伟 ^{[1
]}

吕继东 ^{[2
]}

机构：

[1] 北京交通大学轨道交通控制与安全国家重点实验室

[2] 北京交通大学轨道交通运行控制系统国家工程研究中心

来源：

西南交通大学学报 | 2013年 / 48卷 / 04期

关键词：

CTCS-3级列控系统; 临时限速; 时间自动机; UPPAAL; 实时性;

D O I：

暂无

中图分类号：

U283.4 [信息论与电子计算机的应用];

学科分类号：

082302 ;

摘要：

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

引用

页码：708 / 714

页数：7

共 13 条

[1]

列车运行控制系统分层形式化建模与验证分析.[D].吕继东.北京交通大学.2011, 09

[2]

高速铁路列车运行控制系统的形式化建模与验证方法研究.[D].曹源.北京交通大学.2011, 10

[3]

软件开发的形式化方法.[M].古天龙[著];.高等教育出版社.2005,

[4]

时间自动机及其应用研究.[D].孙全勇.哈尔滨工程大学.2007, 04