摘要
为了满足铁路线路互联互通以及设备故障之后列车降级运行的需求,列车在运行过程中需要进行等级转换.等级转换过程中,车载设备未正常接收转换预告点、转换执行点应答器的信息,或者列车速度未降至线路允许速度以下等因素,可能导致等级转换不成功,因此有必要通过形式化建模对转换过程分析和验证.本文提出了一种基于UPPAAL的等级转换过程建模与验证方法.采用时间自动机理论建立了CTCS-2/CTCS-3等级转换过程的时间自动机网络模型,应用UPPAAL验证工具对等级转换过程进行仿真分析,验证了等级转换过程的安全性,并对现有技术规范提出了改进意见.
In order to meet the interconnection and interoperability of railway lines and downgrade operation of train after equipment failures,level transition is required in the operation process.During transition process,improper receiving of level transition advance point and operation point balise information or unallowable train speed will lead to failure of level transition,which would directly endanger traffic safety.Therefore,it is necessary to analyze and verify transition process through formal modeling.This paper proposes UPPAAL-based modeling and verification methods of level transition process,establishes CTCS-2/CTCS-3 level transition process automata network model based on timed automata theory,which verifies the safety of level transition process.In addition,it puts forward improvement suggestions of the existing technical specifications.
出处
《北京交通大学学报》
CAS
CSCD
北大核心
2012年第6期63-67,73,共6页
JOURNAL OF BEIJING JIAOTONG UNIVERSITY
基金
轨道交通控制与安全国家重点实验室自主课题重点项目资助(RCS2011ZZ001)
轨道交通控制与安全国家重点实验室开放课题项目资助(RCS2011K010)
中央高校基本科研业务费专项资金资助(2012JBM024
2012JBZ014)