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

摘要：

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

关键词：CTCS-3级列控系统、临时限速、时间自动机、UPPAAL、实时性

所属期刊栏目：48

分类号：U283.4(铁路通信、信号)

资助基金：国家863计划资助项目2012AA112801;本文工作得到轨道交通控制与安全国家重点实验室自主课题重点项目RCS2011ZZ001

在线出版日期：2013-10-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：708-714