铁道标准设计2016，Vol.60Issue(10)：126-131,6.DOI:10.13238/j.issn.1004-2954.2016.10.028
基于MSC与UPPAAL的高铁跨界临时限速建模与验证
Modeling and Verification of Cross-border Temporary Speed Restriction for High Speed Railway Based on MSC and UPPAAL
摘要
Abstract
Temporary Speed Restriction Server ( TSRS) is an important part of the High Speed Railway Train Control System, it not only checks the temporary speed restriction orders issued by CTC, but also exchanges information frequently with the temporary speed restriction server of the adjacent dispatching station, and the requirements for its security and real-time performance are rigorous. In order to meet the requirement of the high speed railway train control system, a combination of timed automata theory with Message Sequence Chart ( MSC ) is employed to establish firstly the MSC model of Cross-border Temporary Speed Restriction and timed automata submodel, and then the verification tool of UPPAAL is used to verify the properties of the Cross-border Temporary Speed Restriction System described by BNF syntax. According to the simulation verification results, the security and restricted activity of the Cross-border Temporary Speed Restriction Information are confirmed, which provides an important basis for further development of the Temporary Speed Restriction Server.关键词
临时限速服务器/时间自动机/UPPAAL/实时性/MSCKey words
Temporary Speed Restriction Server/Timed automata/UPPAAL/Real-time/MSC分类
交通工程引用本文复制引用
周翔,武晓春..基于MSC与UPPAAL的高铁跨界临时限速建模与验证[J].铁道标准设计,2016,60(10):126-131,6.基金项目
国家自然科学基金地区项目(61164010) （61164010）
