基于UPPAAL的RBC系统控车流程建模分析

摘要

RBC系统是中国铁路CTCS-3级列控系统中的重要组成部分，LJPPAAL是基于时间自动机理论的实时系统建模分析验证工具，使用UPPAAL分析RBC系统控车流程，可以验证流程的特性，对于保证RBC系统控车流程的安全性有着重要的实际意义。 论文完成的主要工作如下： 1.介绍了时间自动机理论及其模型检验工具UJPPAAL的使用方法。 2.通过分析列车在RBC系统控制下的运行过程，把RBC系统控车流程分为五部分：列车登录流程，正常控车流程，RBC交接流程，列车注销流程和消息重发流程。 3.基于时间自动机理论对RBC系统控车的五个流程以及其他外部设备分别进行了建模：根据研究对象的特点，在合理的抽象和假设之后，确定了各个模型的状态，状态跳转路径和状态跳转的约束条件，得到了RBC系统控车流程的时间自动机模型。 4.使用UPPAAL对RBC系统控车流程的时间自动机模型进行了分析验证：通过设置通道和全局变量，构造了时间自动机的积；使用模拟器，模拟了RBC控制列车运行过程，分析RBC控制列车运行过程中的状态变化；使用验证器，通过快速搜索整个系统的状态空间，验证RBC系统控车流程的活性和正确性等各项特性。

目录

文摘

英文文摘

声明

致谢

1引言

1.1列控系统发展现状

1.1.1国外列控系统现状

1.1.2国内列控系统现状

1.2论文研究的目的和意义

1.3论文章节安排

2分析工具UPPAAL介绍

2.1形式化方法

2.1.1形式化方法概述

2.1.2形式化方法分类

2.1.3形式化方法优点

2.2时间自动机

2.2.1自动机概述

2.2.2时间自动机

2.2.3可达性分析

2.2.4时间自动机优点

2.3模型分析验证工具UPPAAL

2.3.1 UPPAAL结构

2.3.2 UPPAAL理论模型

3RBC系统控车流程分析与设计

3.1 RBC系统介绍

3.1.1 CTCS-3级系统

3.1.2 RBC子系统

3.2 RBC系统控车流程分析设计

3.2.1列车登录流程

3.2.2正常控车流程

3.2.3 RBC交接流程

3.2.4列车注销流程

3.2.5消息重发流程

3.3系统需求

4基于时间自动机的RBC控车流程建模

4.1 RBC控车流程建模

4.1.1列车登录模型

4.1.2正常控车模型

4.1.3 RBC交接模型

4.1.4列车注销模型

4.1.5消息重发模型

4.2外部设备建模

4.2.1列车模型

4.2.2其他地面设备模型

5基于UPPAAL的RBC控车流程验证分析

5.1构造时间自动机的积

5.1.1使用UPPAAL构造时间自动机的积

5.2 RBC消息重发流程分析验证

5.2.1消息重发流程仿真分析

5.2.2消息重发流程验证

5.3 RBC控车流程分析验证

5.3.1 RBC控车流程仿真分析

5.3.2 RBC控车流程验证

6结论与展望

6.1结论

6.2展望

参考文献

作者简历