| 摘要 | 第1-5页 |
| ABSTRACT | 第5-11页 |
| 缩略词 | 第11-12页 |
| 第一章 绪论 | 第12-18页 |
| ·课题研究背景 | 第12-14页 |
| ·国内外研究现状及选题依据 | 第14-16页 |
| ·国内外研究现状 | 第14-15页 |
| ·选题依据 | 第15-16页 |
| ·论文组织结构 | 第16-18页 |
| 第二章 基于状态事件故障树的嵌入式软件安全性分析方法 | 第18-28页 |
| ·软件安全性的需求和设计模型 | 第18-21页 |
| ·状态事件故障树 | 第18-20页 |
| ·状态图 | 第20-21页 |
| ·形式化建模与验证 | 第21-24页 |
| ·模型检测方法 | 第21-22页 |
| ·Promela建模方法 | 第22-24页 |
| ·基于状态事件故障树的软件安全性分析方法 | 第24-27页 |
| ·时序状态事件故障树 | 第25页 |
| ·基于状态事件故障树的嵌入式软件安全性分析框架 | 第25-27页 |
| ·本章小结 | 第27-28页 |
| 第三章 时序状态事件故障树的构建及安全属性规约 | 第28-40页 |
| ·状态事件故障树的时序化扩展 | 第28-32页 |
| ·线性时序逻辑 | 第28-30页 |
| ·逻辑门的时序化规则 | 第30-31页 |
| ·时序状态事件故障树的构建方法 | 第31-32页 |
| ·时序状态事件故障树的约简 | 第32-36页 |
| ·约简规则 | 第33-34页 |
| ·时序状态事件故障树的约简过程 | 第34-36页 |
| ·最小割集的LTL规约 | 第36-39页 |
| ·下行法求解LTL规约 | 第36-38页 |
| ·上行法求解LTL规约 | 第38-39页 |
| ·本章小结 | 第39-40页 |
| 第四章 安全需求到状态图的扩展及安全属性的验证 | 第40-52页 |
| ·状态事件故障树元素到状态图元素的映射 | 第40-41页 |
| ·逻辑门转换规则 | 第41-44页 |
| ·与门的转换 | 第42-43页 |
| ·或门的转换 | 第43-44页 |
| ·优先与门的转换 | 第44页 |
| ·安全需求扩展状态图的构建方法 | 第44-47页 |
| ·安全属性的验证 | 第47-51页 |
| ·安全需求扩展状态图的Promela建模 | 第47-50页 |
| ·最小割集LTL规约的验证 | 第50-51页 |
| ·本章小结 | 第51-52页 |
| 第五章 襟缝翼控制系统实例分析 | 第52-68页 |
| ·襟缝翼控制系统软件FT构建 | 第52-53页 |
| ·襟缝翼控制系统简介 | 第52页 |
| ·襟缝翼控制系统FT建模 | 第52-53页 |
| ·襟缝翼控制系统软件系统LTSEFT构建及约简 | 第53-61页 |
| ·襟缝翼控制系统LTSEFT模块化构建 | 第53-58页 |
| ·襟缝翼控制系统LTSEFT约简 | 第58-61页 |
| ·襟缝翼控制系统软件安全属性提取 | 第61-62页 |
| ·襟缝翼控制系统安全需求扩展状态图的建立 | 第62-64页 |
| ·襟缝翼控制系统安全需求扩展状态图Promela建模与验证 | 第64-67页 |
| ·襟缝翼控制系统Promela建模 | 第64-66页 |
| ·系统安全属性LTL规约的验证与分析 | 第66-67页 |
| ·本章小结 | 第67-68页 |
| 第六章 总结与展望 | 第68-70页 |
| ·论文工作总结 | 第68-69页 |
| ·未来工作展望 | 第69-70页 |
| 参考文献 | 第70-75页 |
| 致谢 | 第75-76页 |
| 在学期间的研究成果及发表的学术论文 | 第76页 |