| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-9页 |
| 目录 | 第9-11页 |
| 1 引言 | 第11-19页 |
| ·选题目的及立题意义 | 第11-13页 |
| ·研究背景简介 | 第13-18页 |
| ·CTCS-3级列车控制系统简介 | 第13-15页 |
| ·国内外形式化建模验证方法的研究现状 | 第15-16页 |
| ·国内外形式化验证工具集成平台研究现状 | 第16-18页 |
| ·论文的研究内容及组织结构 | 第18页 |
| ·本章小结 | 第18-19页 |
| 2 基于UML扩展机制的列控系统需求规范建模方法介绍 | 第19-31页 |
| ·列控系统需求规范建模的需求分析 | 第19-20页 |
| ·UML扩展机制 | 第20-21页 |
| ·面向列控系统需求规范的混成UML概要文件设计 | 第21-28页 |
| ·数据类型概要文件 | 第23-24页 |
| ·表达式与约束概要文件 | 第24-25页 |
| ·通信概要文件 | 第25-26页 |
| ·扩展类概要文件和扩展状态机概要文件 | 第26-28页 |
| ·RSA建模工具 | 第28-30页 |
| ·本章小结 | 第30-31页 |
| 3 列控系统需求规范模型的验证与支持工具集 | 第31-61页 |
| ·列控系统需求规范分析方法体系结构 | 第31-32页 |
| ·列控系统需求模型验证分析阶段的功能需求 | 第32-33页 |
| ·列控系统需求规范验证支持工具的硬件配置和软件工具 | 第33-35页 |
| ·软件约束 | 第34-35页 |
| ·硬件限制 | 第35页 |
| ·列控系统需求规范验证支持工具的功能实现 | 第35-47页 |
| ·主界面 | 第35-37页 |
| ·UML模型元素抽取 | 第37-40页 |
| ·定义待验证问题 | 第40-42页 |
| ·形式化模型的自动化验证 | 第42-47页 |
| ·列控系统需求规范验证支持工具的界面设计 | 第47-57页 |
| ·主界面 | 第47页 |
| ·UML模型元素抽取 | 第47-49页 |
| ·定义待验证问题 | 第49-51页 |
| ·形式化模型的自动化验证 | 第51-57页 |
| ·UML模型到形式化模型的转换规则 | 第57-59页 |
| ·UML模型到NuSMV模型的转换规则 | 第57-58页 |
| ·UML模型到PHAVer模型的转换规则 | 第58-59页 |
| ·本章小结 | 第59-61页 |
| 4 案例分析 | 第61-75页 |
| ·模式转换场景和RBC交接场景介绍 | 第61-62页 |
| ·模式转换场景 | 第61页 |
| ·RBC交接场景 | 第61-62页 |
| ·基于场景的混成UML模型的建立 | 第62-66页 |
| ·类图 | 第62-64页 |
| ·状态机图 | 第64-66页 |
| ·基于场景的混成UML模型在验证支持工具中的应用 | 第66-73页 |
| ·基于场景的混成UML模型的模型元素抽取 | 第66-68页 |
| ·基于场景的待验证问题的定义 | 第68-69页 |
| ·基于场景的形式化模型的自动化验证 | 第69-73页 |
| ·本章小结 | 第73-75页 |
| 5 结论 | 第75-77页 |
| 参考文献 | 第77-81页 |
| 附录A: NuSMV程序描述简介 | 第81-83页 |
| 附录B: PHAVer程序描述简介 | 第83-85页 |
| 表目录 | 第85-87页 |
| 图目录 | 第87-89页 |
| 作者简历 | 第89-93页 |
| 学位论文数据集 | 第93页 |