| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 引言 | 第11-17页 |
| ·选题背景 | 第11页 |
| ·CBTC系统简介 | 第11-13页 |
| ·数据验证的相关研究现状 | 第13-14页 |
| ·轨道交通领域的研究现状 | 第13-14页 |
| ·其他领域的研究现状 | 第14页 |
| ·选题目的和意义 | 第14-15页 |
| ·论文的组织结构和章节安排 | 第15-17页 |
| 2 CBTC系统数据验证的理论基础 | 第17-24页 |
| ·CBTC系统数据验证理论的引入 | 第17-19页 |
| ·CBTC系统数据特点 | 第17-18页 |
| ·CBTC系统数据验证理论的选择 | 第18-19页 |
| ·时间自动机理论 | 第19-21页 |
| ·时间自动机 | 第19-20页 |
| ·时间自动机网络 | 第20-21页 |
| ·模型分析验证工具UPPAAL | 第21-23页 |
| ·UPPAAL的结构简介 | 第21-22页 |
| ·UPPAAL模型及验证方法 | 第22-23页 |
| ·本章小结 | 第23-24页 |
| 3 基于UPPAAL的CBTC系统数据的验证方法 | 第24-51页 |
| ·CBTC系统数据的形式化验证机制 | 第24-25页 |
| ·CBTC系统数据分析 | 第25-32页 |
| ·数据开发与管理 | 第25-28页 |
| ·数据描述 | 第28-29页 |
| ·数据组成 | 第29-32页 |
| ·CBTC系统数据约束条件 | 第32-41页 |
| ·数据约束条件的设计 | 第32-38页 |
| ·数据约束条件的归纳 | 第38-41页 |
| ·CBTC系统数据验证 | 第41-50页 |
| ·主进程模型 | 第42-44页 |
| ·值域关系模型 | 第44-45页 |
| ·参照关系模型 | 第45-48页 |
| ·逻辑关系模型 | 第48-50页 |
| ·本章小结 | 第50-51页 |
| 4 基于UPPAAL的CBTC系统数据验证的应用研究 | 第51-66页 |
| ·数据验证网络的构建 | 第51-53页 |
| ·数据属性的验证关系 | 第51-52页 |
| ·时间自动机网络的构建 | 第52-53页 |
| ·数据验证与分析的应用实现 | 第53-65页 |
| ·值域关系验证 | 第53-56页 |
| ·参照关系验证 | 第56-59页 |
| ·逻辑关系验证 | 第59-62页 |
| ·综合验证 | 第62-65页 |
| ·本章小结 | 第65-66页 |
| 5 总结与展望 | 第66-68页 |
| ·总结 | 第66页 |
| ·展望 | 第66-68页 |
| 参考文献 | 第68-70页 |
| 图索引 | 第70-72页 |
| 表索引 | 第72-73页 |
| 作者简历 | 第73-75页 |
| 学位论文数据集 | 第75页 |