铁道标准设计2018，Vol.62Issue(5)：171-174,179,5.DOI:10.13238/j.issn.1004-2954.201704260003
基于MSC与UPPAAL的区域控制器切换场景建模与验证
Modeling and Verification of Switch Scene of Zone Controller Based on MSC and UPPAAL
杨璐 1陈永刚1
作者信息
- 1. 兰州交通大学自动化与电气工程学院,兰州 730070
- 折叠
摘要
Abstract
The border switch scene of zone controller (ZC) is an important scene of Urban Rail Transit Train Control System. During the switch process, the handover ZC, the takeover ZC and the vehicle interchange information frequently, and the requirements for its security and real-time performances are more stringent. In this paper,a combination of the MSC semi-formalization method is taken as the entry point and the time automaton theory is used to establish the MSC model and the time automaton network model of ZC switch scene to fulfill the safety verification of ZC switch scene function and limited activity. The results show that the ZC border switch control function meets the requirements of the system security and limited activity. Therefore, this modeling and verification method is applicable to modeling and verification of other scenes of the train control system.关键词
列车控制系统/区域控制器/MSC/UPPAAL/安全验证Key words
Train control system/Zone controller/MSC/UPPAAL/Security verification分类
交通工程引用本文复制引用
杨璐,陈永刚..基于MSC与UPPAAL的区域控制器切换场景建模与验证[J].铁道标准设计,2018,62(5):171-174,179,5.
