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

作者: 杨璐陈永刚

关键词: 列车控制系统区域控制器 MSC UPPAAL 安全验证

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

上一篇： 地铁车辆段作业安全保护系统设计研究
下一篇： 高速铁路异物侵限监测网设置范围计算公式的完善

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

作者: 杨璐 陈永刚

关键词: 列车控制系统 区域控制器 MSC UPPAAL 安全验证

作者: 杨璐陈永刚

关键词: 列车控制系统区域控制器 MSC UPPAAL 安全验证