| 摘要 | 第4-5页 |
| Abstract | 第5-6页 |
| 1 绪论 | 第9-14页 |
| 1.1 研究背景及意义 | 第9-10页 |
| 1.2 国内外研究现状 | 第10-12页 |
| 1.2.1 国外研究现状 | 第10-12页 |
| 1.2.2 国内研究现状 | 第12页 |
| 1.3 论文的研究内容和结构 | 第12-14页 |
| 1.3.1 研究内容 | 第12-13页 |
| 1.3.2 论文结构 | 第13-14页 |
| 2 基于 CBTC 的列车自动防护系统 | 第14-22页 |
| 2.1 CBTC 系统简介 | 第14-16页 |
| 2.2 ATP 系统的组成 | 第16页 |
| 2.3 ATP 系统的总体结构 | 第16-17页 |
| 2.4 ATP 系统功能 | 第17-21页 |
| 2.4.1 列车间隔控制 | 第18-20页 |
| 2.4.2 速度监督和超速防护 | 第20-21页 |
| 2.5 本章小结 | 第21-22页 |
| 3 ATP 系统需求规范与验证方法的演化 | 第22-33页 |
| 3.1 形式化方法与传统建模方法的比较 | 第22页 |
| 3.2 形式化方法的主要研究内容 | 第22-23页 |
| 3.3 形式化 B 方法 | 第23-31页 |
| 3.3.1 B 方法简介 | 第23-24页 |
| 3.3.2 B 方法与其他形式化语言的比较 | 第24-25页 |
| 3.3.3 B 方法基础 | 第25-29页 |
| 3.3.4 抽象机 | 第29-31页 |
| 3.4 本章小结 | 第31-33页 |
| 4 基于 UML 的 ATP 系统需求规范建模分析 | 第33-46页 |
| 4.1 统一建模语言 UML | 第33-38页 |
| 4.1.1 UML 的定义 | 第33页 |
| 4.1.2 UML 的语义模型结构 | 第33-34页 |
| 4.1.3 UML 的基本构造 | 第34-35页 |
| 4.1.4 UML 模型图 | 第35-38页 |
| 4.2 ATP 系统需求规范 UML 模型图的形式化描述 | 第38-45页 |
| 4.2.1 类图的 B 方法形式化描述 | 第39-41页 |
| 4.2.2 状态图的 B 方法形式化描述 | 第41-45页 |
| 4.3 本章小结 | 第45-46页 |
| 5 ATP 系统主要功能模型图及检测 | 第46-56页 |
| 5.1 列车间隔控制功能的 UML 模型图 | 第46-47页 |
| 5.2 列车速度监督与超速防护功能的 UML 模型图 | 第47-51页 |
| 5.3 ATP 系统的总体结构 | 第51-52页 |
| 5.4 系统的模型检测 | 第52-55页 |
| 5.5 本章小结 | 第55-56页 |
| 结论 | 第56-57页 |
| 致谢 | 第57-58页 |
| 参考文献 | 第58-61页 |
| 攻读学位期间的研究成果 | 第61页 |
