| 摘要 | 第2-3页 |
| Abstract | 第3页 |
| 1. 绪论 | 第7-18页 |
| 1.1. 研究背景 | 第7-16页 |
| 1.1.1. 需求验证的必要性 | 第7-8页 |
| 1.1.2. 航天嵌入式软件的实时性要求 | 第8-10页 |
| 1.1.3. 航天嵌入式软件验证技术发展趋势 | 第10-13页 |
| 1.1.4. 国内外研究现状 | 第13-16页 |
| 1.2. 研究目的与意义 | 第16页 |
| 1.3. 研究内容与文章结构 | 第16-18页 |
| 2. 需求验证方法研究 | 第18-34页 |
| 2.1. 需求验证方法论 | 第18-23页 |
| 2.1.1. 形式化的方法 | 第18-20页 |
| 2.1.2. 形式化方法的发展与应用 | 第20页 |
| 2.1.3. 基于模型的检测方法 | 第20-22页 |
| 2.1.4. 模型检测的应用 | 第22-23页 |
| 2.2. 常见需求验证工具 | 第23-26页 |
| 2.2.1. 几种模型检测方案 | 第23-25页 |
| 2.2.2. 工具综合对比 | 第25-26页 |
| 2.3. RTCTL（Real-Time Computation Tree Logic）逻辑 | 第26-32页 |
| 2.3.1. 计算树逻辑CTL | 第26-29页 |
| 2.3.2. Kripke结构 | 第29-30页 |
| 2.3.3. RTCTL语义 | 第30-32页 |
| 2.4. 本章小结 | 第32-34页 |
| 3. 基于Kripke结构的实时性语义改进 | 第34-46页 |
| 3.1. Kripke结构的改进 | 第34-39页 |
| 3.1.1. Kripke结构时间性的不足 | 第34-35页 |
| 3.1.2. 实时Kripke结构RTKS | 第35-37页 |
| 3.1.3. 实时Kripke结构RTKS’ | 第37-39页 |
| 3.2. 对Nu SMV的改进 | 第39-44页 |
| 3.2.1. Nu SMV语言结构与语义 | 第39-40页 |
| 3.2.2. Nu SMV的扩展 | 第40-44页 |
| 3.2.3. 与基于传统Kripke模型的Nu SMV的比较 | 第44页 |
| 3.3. 本章小结 | 第44-46页 |
| 4. 需求模型的建立与转换 | 第46-59页 |
| 4.1. 需求建模语言研究 | 第46-49页 |
| 4.1.1. UML概述 | 第46-47页 |
| 4.1.2. UML视图介绍 | 第47-49页 |
| 4.2. UML模型转换的必要性 | 第49页 |
| 4.3. 需求模型的验证流程 | 第49-51页 |
| 4.4. UML建模过程 | 第51-52页 |
| 4.5. UML模型到RTSMV的转换规范 | 第52-58页 |
| 4.5.1. UML模型的转换原则 | 第52页 |
| 4.5.2. UML模型到RTSMV语义转换的形式化映射 | 第52-55页 |
| 4.5.3. 类图转换规则约定 | 第55-56页 |
| 4.5.4. 状态图转换约定 | 第56-58页 |
| 4.6. 本章小结 | 第58-59页 |
| 5. 航天嵌入式软件应用验证 | 第59-68页 |
| 5.1. 一级关机模型 | 第59-62页 |
| 5.1.1. 需求描述 | 第59页 |
| 5.1.2. 需求的UML建模 | 第59-61页 |
| 5.1.3. 模型转换与验证结果 | 第61-62页 |
| 5.2. 安全自毁模型 | 第62-66页 |
| 5.2.1. 需求描述 | 第62页 |
| 5.2.2. 需求的UML建模 | 第62-64页 |
| 5.2.3. 模型转换与验证结果 | 第64-66页 |
| 5.3. 本章小结 | 第66-68页 |
| 6. 总结与展望 | 第68-69页 |
| 6.1. 总结 | 第68页 |
| 6.2. 展望 | 第68-69页 |
| 参考文献 | 第69-72页 |
| 攻读硕士学位期间发表学术论文情况 | 第72-73页 |
| 致谢 | 第73-74页 |
