北京交通大学学报2012，Vol.36Issue(6)：63-67,73,6.
基于UPPAAL的高铁列控系统等级转换过程建模与验证
UPPAAL-based modeling and verification of level transition process of high-speed railway train control system
摘要
Abstract
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.关键词
CTCS-2/CTCS-3等级转换/时间自动机/UPPAAL/安全性Key words
level transition between CTCS-2 and CTCS-3/ timed automata/ UPPAAL/ safety分类
交通工程引用本文复制引用
康仁伟,王俊峰,吕继东..基于UPPAAL的高铁列控系统等级转换过程建模与验证[J].北京交通大学学报,2012,36(6):63-67,73,6.基金项目
轨道交通控制与安全国家重点实验室自主课题重点项目资助(RCS2011ZZ001) （RCS2011ZZ001）
轨道交通控制与安全国家重点实验室开放课题项目资助(RCS2011K010) （RCS2011K010）
中央高校基本科研业务费专项资金资助(2012JBM024,2012JBZ014) （2012JBM024,2012JBZ014）
