| 摘要 | 第1-4页 |
| ABSTRACT | 第4-8页 |
| 1 前言 | 第8-13页 |
| ·研究背景和意义 | 第8-9页 |
| ·研究现状 | 第9-10页 |
| ·主要研究内容 | 第10-13页 |
| 2 系统建模 | 第13-25页 |
| ·模型检测的介绍 | 第13-14页 |
| ·统一建模语言UML顺序图 | 第14-16页 |
| ·UML介绍 | 第14页 |
| ·UML顺序图 | 第14-15页 |
| ·UML顺序图的扩展 | 第15-16页 |
| ·实现工具UPPAAL | 第16-20页 |
| ·UPPAAL介绍 | 第16-17页 |
| ·UPPAAL的检测步骤 | 第17-19页 |
| ·UPPAAL的检测语法 | 第19-20页 |
| ·时间自动机模型的理论基础 | 第20-23页 |
| ·有时间约束的转换系统 | 第20-21页 |
| ·时间自动机的语法和语义 | 第21页 |
| ·时间自动机积的构造 | 第21-23页 |
| ·UML顺序图到时间自动机模型的转换 | 第23-25页 |
| 3 系统性质 | 第25-32页 |
| ·计算树时态逻辑CTL* | 第25-27页 |
| ·CTL和LTL | 第27-30页 |
| ·LTL | 第27-28页 |
| ·CTL | 第28-30页 |
| ·CTL和LTL的模型检测算法 | 第30-32页 |
| ·CTL的模型检测算法 | 第30页 |
| ·LTL的模型检测算法 | 第30-32页 |
| 4 运营场景的安全验证 | 第32-45页 |
| ·CTCS-3级列控系统简介 | 第32页 |
| ·CTCS-3运营场景之RBC切换 | 第32-34页 |
| ·RBC切换场景的建模 | 第34-43页 |
| ·建立RBC切换场景的UML模型 | 第34-37页 |
| ·建立RBC切换场景的UPPAAL模型-时间自动机网络 | 第37-43页 |
| ·RBC切换场景的安全验证分析 | 第43-45页 |
| 5 基于BDD的全符号化的可达性算法 | 第45-72页 |
| ·已有的半符号化可达性分析方法 | 第45-49页 |
| ·域自动机 | 第45-46页 |
| ·带自动机 | 第46-49页 |
| ·基于BDD的全符号化可达性算法 | 第49-63页 |
| ·BDD存储结构理论 | 第49-53页 |
| ·一种时间约束的BDD存储结构——DDD结构 | 第53-59页 |
| ·单时间自动机的可达性分析算法 | 第59-60页 |
| ·多时间自动机的可达性分析算法 | 第60-63页 |
| ·全符号化的可达性分析算法实例 | 第63-72页 |
| 总结与展望 | 第72-73页 |
| 参考文献 | 第73-77页 |
| 致谢 | 第77-78页 |
| 攻读学位期间发表的学术论文目录 | 第78页 |
| 攻读学位期间参加的科研项目 | 第78-79页 |