基于MSC与UPPAAL的列控系统等级转换场景形式化验证

• 作者: 胡雪莲 陶彩霞
• 来源期刊: 铁道标准设计
• 学科: 交通运输
• 关键词: CTCS 等级转换 MSC 时间自动机 UPPAAL 建模
• 年，卷（期）: 2015,（2）
• 所属期刊栏目: 通信/信号
• 页码范围: 122-127
• 页数: 6页
• 分类号: U285.21
• 字数: 4080字
• 语种: 中文
• DOI: 10.13238/j.issn.1004-2954.2015.02.030

摘要

等级转换是C3级列控系统的重要场景，是列控系统兼容性的集中体现，转换的成功与否直接关系到列车的运行安全和行车效率。因此，有必要对设计规范中所描述的转换过程进行形式化建模和验证，以保障系统的安全性和实时性。为保证设计规范与所建模型的一致性，采取消息顺序图( MSC)与时间自动机相结合的方式，建立等级转换场景中C2级向C3级转换过程的MSC模型，并将其转换为时间自动机模型。应用UPPAAL对模型的安全性和受限活性进行仿真验证，结果表明设计规范中所描述的转换过程是安全可靠的，可以满足C3级列控系统的兼容性和安全性要求。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陶彩霞	兰州交通大学自动化与电气工程学院	54	201	8.0	12.0
2	胡雪莲	兰州交通大学自动化与电气工程学院	1	9	1.0	1.0