CTCS-3级列控系统车地交互流程形式化建模与验证

正在建设的时速300 km/h以上的高速铁路已采用CTCS-3级列车运行控制系统.车地信息交互流程是影响CTCS-3级列控系统的效率、可靠性和安全性的主要因素之一.基于时间自动机理论对车地交互流程进行建模与验证具有重要意义.首先将车地交互流程分为4个典型的子流程：任务启动流程、正常行车流程、RBC切换流程和任务结束流程,然后针对这些子流程建立无线闭塞中心（RBC）、车载设备（ATP）和铁路专用移动通信网（GSM-R）的时间自动机网络模型,最后利用时间自动机模型验证工具UPPAAL进行仿真分析,验证了CTCS-3级列控系统的车地交互流程的安全性和受限活性.

Formal modeling and checking of procedure message exchange between train-ground for CTCS level 3

It is confirmed that the chinese train control system（CTCS） level 3 is adopted in newly-built railway lines,where the train speed is expected to exceed 300 kilometers per hour.Procedure message exchange between train and ground is one of the most significant factors that affect the transportation efficiency,reliability and safety of the CTCS level 3.It is very important to use time automata for formal modeling and checking of procedure message exchange between train and ground.Firstly,we divide procedure message exchange between train and ground there are four typical sub-procedures between train and ground： procedure start of mission,procedure train movement,procedure RBC handover,procedure end of mission.Secondly,the time automata models of RBC,ATP and GSM-R are established according to the procedures.Finally,the formal analysis by the UPPAAL tool show that the procedure message exchange between train and ground is provided with security and restricted activity.