| 中文摘要 | 第1-8页 |
| ABSTRACT | 第8-10页 |
| 目录 | 第10-12页 |
| 第一章 绪论 | 第12-22页 |
| ·选题的背景 | 第12-13页 |
| ·列车运行控制系统安全技术的演变和发展 | 第13-17页 |
| ·列车运行控制系统发展初期和故障——安全概念的产生 | 第13页 |
| ·列车运行控制系统的电气化和故障安全技术的发展 | 第13-14页 |
| ·计算机时代的列车运行控制系统和安全性技术的应用 | 第14-16页 |
| ·列车运行控制系统安全性设计遇到的挑战 | 第16-17页 |
| ·形式化方法的发展和应用情况 | 第17-20页 |
| ·选题的目的和意义 | 第20页 |
| ·论文的主要研究工作和篇章结构 | 第20-22页 |
| 第二章 形式化建模和模型检验方法 | 第22-32页 |
| ·形式化建模和验证方法的选择 | 第22-24页 |
| ·形式化建模方法的选择 | 第22-23页 |
| ·形式化验证方法的选择 | 第23-24页 |
| ·基于自动机理论的模型检验方法 | 第24-26页 |
| ·Partial order技术 | 第25页 |
| ·on-the-fly 技术 | 第25-26页 |
| ·二叉判定图和符号模型检验 | 第26页 |
| ·模型检验的优化技术 | 第26-28页 |
| ·实时系统模型检验方法 | 第28-31页 |
| ·离散实时系统模型检验 | 第29页 |
| ·连续实时系统模型检验 | 第29-31页 |
| ·本章小结 | 第31-32页 |
| 第三章 时间自动机网络模型及其模型检验方法研究 | 第32-51页 |
| ·经典自动机模型的局限性 | 第32-33页 |
| ·时间自动机网络模型 | 第33-37页 |
| ·时间自动机网络模型的形式化定义 | 第35-36页 |
| ·时间自动机网络模型的形式化描述语言 | 第36-37页 |
| ·基于时间自动机网络的模型检验方法 | 第37-49页 |
| ·组件自动机转换为带有时钟状态的有限自动机 | 第37-43页 |
| ·组件自动机的同步积复合 | 第43-44页 |
| ·时间自动机网络转换为 Kripke结构 | 第44-45页 |
| ·用 TCTL公式表示所要验证的系统属性 | 第45-46页 |
| ·模型检验算法 | 第46-49页 |
| ·本章小结 | 第49-51页 |
| 第四章 形式化设计验证方法研究 | 第51-60页 |
| ·形式化设计建模 | 第51-54页 |
| ·形式化验证 | 第54-57页 |
| ·形式化开发 | 第57-59页 |
| ·本章小结 | 第59-60页 |
| 第五章 大连快轨3号线 ATP车载设备的形式化设计与验证 | 第60-85页 |
| ·系统需求 | 第60-61页 |
| ·ATP车载设备需求分析 | 第61页 |
| ·系统功能 | 第61-64页 |
| ·形式化设计和验证 | 第64-84页 |
| ·需求分析 | 第64-66页 |
| ·形式化建模和设计 | 第66-71页 |
| ·形式化验证 | 第71-76页 |
| ·形式化开发 | 第76-84页 |
| ·本章小结 | 第84-85页 |
| 第六章 结论 | 第85-88页 |
| ·论文总结 | 第85-86页 |
| ·展望 | 第86-88页 |
| 参考文献 | 第88-95页 |
| 附录 A ATP车载控制系统实时性模型描述程序 | 第95-101页 |
| 作者简历 | 第101-102页 |
| 博士研究生期间发表论文目录 | 第102-104页 |