| 致谢 | 第1-6页 |
| 中文摘要 | 第6-8页 |
| ABSTRACT | 第8-10页 |
| 目录 | 第10-13页 |
| 术语表 | 第13-15页 |
| 1 引言 | 第15-25页 |
| ·选题背景 | 第15-17页 |
| ·问题的提出 | 第15-16页 |
| ·基本概念 | 第16-17页 |
| ·列控系统的特点及规范质量 | 第17-19页 |
| ·列控系统的特点 | 第17-18页 |
| ·列控系统规范质量 | 第18-19页 |
| ·列控系统需求规范建模与验证方法的演化 | 第19-21页 |
| ·传统的建模与验证方法 | 第19-20页 |
| ·形式化建模与验证方法的形成 | 第20页 |
| ·多技术手段集成方法在建模与验证中的发展 | 第20-21页 |
| ·选题意义和目的 | 第21-22页 |
| ·论文主要内容与篇章结构 | 第22-25页 |
| 2 列控系统需求规范建模与验证研究现状 | 第25-33页 |
| ·列控系统需求规范建模方法 | 第25-28页 |
| ·基于统一建模语言的建模方法 | 第25-26页 |
| ·基于自动机理论的建模方法 | 第26-27页 |
| ·基于Petri网的建模方法 | 第27-28页 |
| ·其它建模方法 | 第28页 |
| ·列控系统需求规范验证方法 | 第28-31页 |
| ·定理证明 | 第29-30页 |
| ·模型检验 | 第30-31页 |
| ·研究现状总结与分析 | 第31-33页 |
| ·研究情况总结 | 第31-32页 |
| ·研究现状分析 | 第32-33页 |
| 3 列控系统需求规范建模与验证方法 | 第33-43页 |
| ·方法概述 | 第33-35页 |
| ·方法的实现 | 第35-41页 |
| ·本章小结 | 第41-43页 |
| 4 基于扩展UML的列控系统需求规范建模与分析 | 第43-77页 |
| ·UML及其扩展机制 | 第43-49页 |
| ·UML的特点及其视图 | 第43-48页 |
| ·UML扩展机制 | 第48-49页 |
| ·对象约束语言OCL | 第49页 |
| ·列控系统需求规范UML模型的形式语法和语义定义 | 第49-55页 |
| ·类图、对象图和部署图的语法 | 第50-51页 |
| ·状态图的语法和语义 | 第51-53页 |
| ·序列图的语法和语义 | 第53-55页 |
| ·活动图的语法和语义 | 第55页 |
| ·UML构建列控系统安全模型 | 第55-63页 |
| ·安全苛求系统模型的UML扩展需求 | 第56-57页 |
| ·基于扩展UML的列控系统需求规范安全模型构建方法 | 第57-62页 |
| ·列控系统需求规范安全模型模板 | 第62-63页 |
| ·建模及模型检查规则 | 第63-74页 |
| ·规则的定义 | 第64-74页 |
| ·规则的正确性分析 | 第74页 |
| ·本章小结 | 第74-77页 |
| 5 列控系统需求规范模型转换及规则证明 | 第77-103页 |
| ·模型转换相关的概念 | 第77-79页 |
| ·模型转换框架 | 第79-80页 |
| ·元模型及转换规则 | 第80-92页 |
| ·UML元模型 | 第80-84页 |
| ·CSP元模型 | 第84-85页 |
| ·UML到CSP的转换规则 | 第85-92页 |
| ·模型转换中特性的保持与转换规则的证明 | 第92-98页 |
| ·模型转换中特性的保持 | 第93-94页 |
| ·模型转换规则的证明 | 第94-98页 |
| ·验证模型的约简与验证结果分析 | 第98-101页 |
| ·验证模型的约简方法 | 第98-99页 |
| ·验证结果分析 | 第99-101页 |
| ·本章小结 | 第101-103页 |
| 6 软件工具的开发与案例分析 | 第103-121页 |
| ·规范建模与验证软件工具的开发 | 第103-104页 |
| ·案例分析1：CTCS-3级列控系统模式转换规范的建模与验证 | 第104-114页 |
| ·CTCS-3级列控车载设备工作模式 | 第104-105页 |
| ·模式转换规范的建模 | 第105-113页 |
| ·模式转换规范的模型转换及形式化验证 | 第113-114页 |
| ·案例分析2：“任务开始”流程规范的建模与验证 | 第114-119页 |
| ·“任务开始”流程概述 | 第114-115页 |
| ·“任务开始”流程的建模 | 第115-117页 |
| ·“任务开始”流程的模型转换及形式化验证 | 第117-119页 |
| ·本章小结 | 第119-121页 |
| 7 结论 | 第121-123页 |
| ·研究成果 | 第121页 |
| ·论文创新点 | 第121-122页 |
| ·展望 | 第122-123页 |
| 参考文献 | 第123-127页 |
| 附录A | 第127-133页 |
| 附录B | 第133-135页 |
| 附录C | 第135-139页 |
| 作者简历 | 第139-143页 |
| 学位论文数据集 | 第143页 |