铁道标准设计Issue(2)：122-127,6.DOI:10.13238/j.issn.1004-2954.2015.02.030
基于MSC与UPPAAL的列控系统等级转换场景形式化验证
Formal Verification of Level Transition Process in Train Control System Based On MSC and UPPAAL
胡雪莲 1陶彩霞1
作者信息
- 1. 兰州交通大学自动化与电气工程学院，兰州 730070
- 折叠
摘要
Abstract
Level transition is one of the most important scenarios in CTCS-3 control system and the very reflection of its compatibility. The successful transition is directly related to train operation safety and transportation efficiency. Therefore, in order to guarantee the security and real-time performance of the system, it is necessary to formally build and verify a model of transition process described in the design specification. To ensure the consistency between of the design specification, the message sequence configure ( MSC) is combined with timed automata, the MSC model is established for C2 to C3 transition process in level transition scenario and is transformed to timed automata model. Then the security and restricted activity of the model are simulated and verified by applying UPPAAL validation tool. The results show that the transition process described in the design specification is safe and reliable to meet the requirements of compatibility and security in CTCS-3 system.关键词
CTCS/等级转换/MSC/时间自动机/UPPAAL/建模Key words
CTCS/Level transition/MSC/Timed automata/UPPAAL/Modeling分类
交通工程引用本文复制引用
胡雪莲,陶彩霞..基于MSC与UPPAAL的列控系统等级转换场景形式化验证[J].铁道标准设计,2015,(2):122-127,6.
