北京交通大学学报2011，Vol.35Issue(2)：76-81,6.
CTCS-3级列控系统车地交互流程形式化建模与验证
Formal modeling and checking of procedure message exchange between train-ground for CTCS level 3
摘要
Abstract
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.关键词
列车运行控制系统/车地信息交互流程/形式化建模与验证/时间自动机Key words
chinese train control system(CTCS)/ procedure message exchange between train and ground/ formal modeling and checking/ time automata分类
信息技术与安全科学引用本文复制引用
刘中田,吕继东,孙伟亮..CTCS-3级列控系统车地交互流程形式化建模与验证[J].北京交通大学学报,2011,35(2):76-81,6.基金项目
国家"863"计划项目资助(0912JJ0104-XH00-H-HZ-00 1-20100419) （0912JJ0104-XH00-H-HZ-00 1-20100419）
北京交通大学科技基金项目资助(2007XM004) （2007XM004）
