基于UPPAAL的高铁列控系统等级转换过程建模与验证

UPPAAL-based modeling and verification of level transition process of high-speed railway train control system

为了满足铁路线路互联互通以及设备故障之后列车降级运行的需求,列车在运行过程中需要进行等级转换.等级转换过程中,车载设备未正常接收转换预告点、转换执行点应答器的信息,或者列车速度未降至线路允许速度以下等因素,可能导致等级转换不成功,因此有必要通过形式化建模对转换过程分析和验证.本文提出了一种基于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.