基于MSC与UPPAAL的区域控制器切换场景建模与验证

• 作者: 杨璐 陈永刚
• 来源期刊: 铁道标准设计
• 学科: 交通运输
• 关键词: 列车控制系统 区域控制器 MSC UPPAAL 安全验证
• 年，卷（期）: 2018,（5）
• 所属期刊栏目: 通信/信号
• 页码范围: 171-174,179
• 页数: 5页
• 分类号: U285.21
• 字数: 3471字
• 语种: 中文
• DOI: 10.13238/j.issn.1004-2954.201704260003

摘要

区域控制器(Zone Controller,ZC)边界切换场景是城市轨道交通列车控制系统的重要场景,切换过程中移交ZC、接管ZC和车载子系统之间要进行频繁的信息交互,因而对其安全性和实时性有更严苛的要求.根据ZC子系统特点,将MSC半形式化方法作为切入点,结合时间自动机理论,建立ZC切换场景的MSC模型和时间自动机网络模型,用于ZC切换场景功能和受限活性的安全验证.结果表明:ZC边界切换控制功能满足系统安全性和受限活性的规范要求.因此此种建模验证方法是可行的,可以将其应用于列控系统其他场景的建模与验证过程中.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈永刚	兰州交通大学自动化与电气工程学院	50	213	8.0	11.0
2	杨璐	兰州交通大学自动化与电气工程学院	3	4	1.0	2.0