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

• 作者: 周翔 武晓春
• 来源期刊: 铁道标准设计
• 学科: 交通运输
• 关键词: 临时限速服务器 时间自动机 UPPAAL 实时性 MSC
• 年，卷（期）: 2016,（10）
• 所属期刊栏目: 通信/信号
• 页码范围: 126-131
• 页数: 6页
• 分类号: U284.48+2
• 字数: 3996字
• 语种: 中文
• DOI: 10.13238/j.issn.1004-2954.2016.10.028

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	武晓春	兰州交通大学自动化与电气工程学院	50	190	8.0	12.0
2	周翔	兰州交通大学自动化与电气工程学院	3	14	3.0	3.0