| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 引言 | 第11-22页 |
| ·研究背景 | 第11-12页 |
| ·研究意义 | 第12-13页 |
| ·研究现状 | 第13-15页 |
| ·列控系统规范建模与验证的方法 | 第15-20页 |
| ·论文主要工作 | 第20页 |
| ·论文结构安排 | 第20-22页 |
| 2 系统规范建模验证基础 | 第22-34页 |
| ·UML概述 | 第22-27页 |
| ·UML的定义和构成 | 第22-23页 |
| ·UML的建模机制及图形 | 第23-27页 |
| ·HybridUML概述 | 第27-30页 |
| ·UML扩展机制 | 第27-28页 |
| ·HybridUML扩展基础 | 第28-30页 |
| ·微分动态逻辑概述 | 第30-31页 |
| ·软件RSA和KeYmaera | 第31-33页 |
| ·建模软件Rational Software Architect(RSA) | 第31-32页 |
| ·验证软件KeYmaera | 第32-33页 |
| ·本章小结 | 第33-34页 |
| 3 系统规范的HybridUML建模 | 第34-50页 |
| ·HybridUML在RSA中的实现 | 第34-47页 |
| ·基本包 | 第34-35页 |
| ·类型包 | 第35-37页 |
| ·数据包 | 第37-38页 |
| ·表达式包 | 第38-41页 |
| ·扩展类(Agent)和扩展状态机(Mode)包 | 第41-46页 |
| ·HybridUML概要文件的组织 | 第46-47页 |
| ·HybridUML模型的建立 | 第47-49页 |
| ·本章小结 | 第49-50页 |
| 4 系统规范模型的形式化验证 | 第50-56页 |
| ·HybridUML模型到微分动态逻辑模型的转换 | 第50-53页 |
| ·验证结果分析 | 第53-55页 |
| ·本章小结 | 第55-56页 |
| 5 RBC切换流程建模与验证 | 第56-70页 |
| ·RBC切换流程 | 第56-57页 |
| ·RBC切换的HybridUML模型 | 第57-62页 |
| ·类图 | 第57-60页 |
| ·状态机图 | 第60-62页 |
| ·RBC切换的微分动态逻辑模型 | 第62-66页 |
| ·形式化验证及分析 | 第66-69页 |
| ·初始约束条件和微分不变量 | 第66-67页 |
| ·关键参数分析 | 第67-68页 |
| ·模型验证 | 第68-69页 |
| ·本章小结 | 第69-70页 |
| 6 结论和展望 | 第70-72页 |
| ·结论 | 第70页 |
| ·展望 | 第70-72页 |
| 参考文献 | 第72-75页 |
| 图索引 | 第75-77页 |
| 表索引 | 第77-78页 |
| 作者简历 | 第78-80页 |
| 学位论文数据集 | 第80页 |