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

作     者：袁磊 王俊峰 康仁伟 吕继东 YUAN Lei;WANG Junfeng;KANG Renwei;Lü Jidong

作者机构：北京交通大学轨道交通控制与安全国家重点实验室北京100044 北京交通大学轨道交通运行控制系统国家工程研究中心北京100044 

出 版 物：《西南交通大学学报》 (Journal of Southwest Jiaotong University)

年 卷 期：2013年第48卷第4期

页      面：708-714页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家863计划资助项目(2012AA112801) 轨道交通控制与安全国家重点实验室自主课题重点项目(RCS2011ZZ001)的资助 

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

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