基于MSC与UPPAAL的高铁跨界临时限速建模与验证

作     者：周翔 武晓春 ZHOU Xiang;WU Xiao-chun

作者机构：兰州交通大学自动化与电气工程学院兰州730070 

基　　金：国家自然科学基金地区项目(61164010) 

出 版 物：《铁道标准设计》 (Railway Standard Design)

年 卷 期：2016年第60卷第10期

页      码：126-131页

摘      要：临时限速服务器是高铁列控系统的重要组成部分,其不仅要校验CTC下发的临时限速命令,还要与相邻调度台临时限速服务器之间进行频繁的信息交互,因此对其安全性和实时性要求也更苛刻。为了满足高铁列控系统对其运行的要求,采用时间自动机理论和消息顺序图(MSC)相结合的方法,首先建立跨界临时限速命令的MSC模型和时间自动机子模型,再利用UPPAAL验证工具对形式化语法BNF描述的时间自动机子模型属性进行验证。根据仿真验证结果确认了跨界临时限速信息的安全性和受限活性,为进一步开发临时限速服务器功能提供了重要的依据。

主 题 词：临时限速服务器 时间自动机 UPPAAL 实时性 MSC 

学科分类：08[工学] 082302[082302] 0823[工学-农业工程类] 

D　O　I：10.13238/j.issn.1004-2954.2016.10.028

馆 藏 号：203189970...