基于Timed-UML顺序图的RBC交接形式化建模与分析

• 作者: 安越 李国宁
• 来源期刊: 铁道标准设计
• 学科: 交通运输
• 关键词: 车载系统 RBC交接 实时UML顺序图 时间自动机
• 年，卷（期）: 2016,（6）
• 所属期刊栏目: 通信/信号
• 页码范围: 132-137,138
• 页数: 7页
• 分类号: U284.48
• 字数: 5861字
• 语种: 中文
• DOI: 10.13238/j.issn.1004-2954.2016.06.027

摘要

在CTCS-3级列控系统中,采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时,控制权将会移交至前方相邻RBC,整个过程称为RBC交接。在运行中,RBC交接过程能否实时安全可靠地执行,直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发,建立切换的Timed-UML顺序图模型,然后按照UML-TA转换规则,建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析,对模型的死锁和功能实现做了验证,从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李国宁	兰州交通大学自动化与电气工程学院	48	149	7.0	8.0
2	安越	兰州交通大学自动化与电气工程学院	1	7	1.0	1.0