原文传递
基于UPPAAL的RBC系统控车流程建模分析
| 论文题名： | 基于UPPAAL的RBC系统控车流程建模分析 |
| 关键词： | RBC系统;UPPAAL;控车流程;建模分析 |
| 摘要： | RBC系统是中国铁路CTCS-3级列控系统中的重要组成部分，LJPPAAL是基于时间自动机理论的实时系统建模分析验证工具，使用UPPAAL分析RBC系统控车流程，可以验证流程的特性，对于保证RBC系统控车流程的安全性有着重要的实际意义。 论文完成的主要工作如下： 1.介绍了时间自动机理论及其模型检验工具UJPPAAL的使用方法。 2.通过分析列车在RBC系统控制下的运行过程，把RBC系统控车流程分为五部分：列车登录流程，正常控车流程，RBC交接流程，列车注销流程和消息重发流程。 3.基于时间自动机理论对RBC系统控车的五个流程以及其他外部设备分别进行了建模：根据研究对象的特点，在合理的抽象和假设之后，确定了各个模型的状态，状态跳转路径和状态跳转的约束条件，得到了RBC系统控车流程的时间自动机模型。 4.使用UPPAAL对RBC系统控车流程的时间自动机模型进行了分析验证：通过设置通道和全局变量，构造了时间自动机的积；使用模拟器，模拟了RBC控制列车运行过程，分析RBC控制列车运行过程中的状态变化；使用验证器，通过快速搜索整个系统的状态空间，验证RBC系统控车流程的活性和正确性等各项特性。 |
| 作者： | 谭耿 |
| 专业： | 交通信息工程及控制 |
| 导师： | 邱宽民 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2008 |
| 正文语种： | 中文 |
检索历史
应用推荐
