基于时间自动机的列控系统数据验证模型的构建与应用

目录

声明

致谢

1 引言

1.1 研究背景及意义

1.2 数据验证研究现状

1.2.1 轨道交通领域的研究现状

1.2.2 其他领域的研究现状

1.3 论文的组织架构

2 相关理论知识和技术简介

2.1 CBTC系统的介绍

2.2 CBTC系统数据验证理论研究

2.2.1 CBTC系统数据特点

2.2.2 数据验证方法的选择

2.3 时间自动机

2.3.1 时间自动机语义

2.3.2 时间自动机网络

2.4 模型验证工具介绍——UPPAAL

2.5 脚本语言Lua简介

2.6 CBTC系统数据的形式化验证机制

2.7 本章小结

3 CBTC系统数据验证的数据设计

3.1 数据分析

3.1.1 数据开发过程

3.1.2 数据描述

3.2 数据约束规则

3.2.1 数据约束规则的设计

3.2.2 数据约束规则的归纳

3.3 本章小结

4 CBTC系统数据总体设计

4.1 CBTC系统数据验证模型设计

4.1.1 主进程模型

4.1.2 值域关系模型

4.1.3 关联关系模型

4.1.4 网络拓扑关系模型

4.2 CBTC系统数据模型验证

4.2.1 数据验证网络的构建

4.2.2 数据验证与分析

4.3 系统功能模块设计

4.4 本章小结

5 CBTC系统数据验证系统的设计与实现

5.1 验证系统框架概要

5.2 数据处理模块详细设计与实现

5.3 约束规则模块设计与实现

5.3.1 值域关系规则的设计与实现

5.3.2 关联关系规则的设计与实现

5.3.3 网络拓扑关系规则的设计与实现

5.4 数据验证模块设计与实现

5.5 结果生成模块的设计与实现

5.6 本章小结

6.1 数据准备

6.2 系统运行

6.3 结果分析

6.4 本章小结

7 总结与展望

7.1 总结

7.2 展望

参考文献

作者简历及攻读硕士/博士学位期间取得的研究成果

独创性声明

学位论文数据集