基于UML顺序图与UPPAAL的列车追踪模块建模研究（英文）

论文摘要

区域控制器(zone controller, ZC)是一个实时复杂系统,它要求过程控制的准确性。列车追踪场景是城市轨道交通(communication based train control, CBTC)系统中ZC的一个重要功能。在对系统进行深层次的开发设计过程中需要对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性。通过分析ZC系统结构及列车追踪分界点处理过程,给出满足系统安全性的功能要求和性能要求,并采用统一建模语言(unified modeling language, UML)与时间自动机相结合的方式建立列车追踪场景中列车筛选和列车追踪分界点的时间自动机网络模型。同时,应用UPPAAL验证工具对系统进行仿真模拟,验证了系统的功能和性能要求。结果表明,列车追踪分界点功能满足系统安全性和受限活性的规范要求。因此,此种建模方法是可行的,可以将其应用于列控系统其他场景的建模与验证过程中。

论文目录

• 0 Introduction
• 1 Train tracking
•   1.1 Train-filter process
•   1.2 Train tracing demarcation-point process
•     （1） Setting the state of demarcation-point.
•     （2） Dealing with demarcation-point with the state of RUT.
•     （3） Dealing with demarcation-point with the state of NRT.
•     （4） Cleaning the traces of demarcation-point with the state of NRT.
•     （5） Dealing with the effect on train.
• 2 UML sequence diagram of train tracking model
• 3 UPPAAL model of train tracking
•   3.1 Timed automata and UPPAAL
•   3.2 UPPAAL model of train-filter
•   3.3 UPPAAL model of train tracking demarcation-point
• 4 Simulation and verification of model
•   4.1 Requirements of train-filter model
•   4.2 Requirements of train tracking demarcation-point model
• 5 Conclusion

文章来源

类型: 期刊论文

作者: 陈永刚,杨璐,王栋

关键词: 列车追踪,系统,区域控制器,时间自动机

来源: Journal of Measurement Science and Instrumentation 2019年02期

年度: 2019

分类: 工程科技Ⅱ辑

专业: 铁路运输

单位: 兰州交通大学自动化与电气工程学院,兰州交通大学机电工程学院

分类号: U284.48

页码: 157-167

总页数: 11

文件大小: 4844K

下载量: 173