基于故障树的航电软件系统安全性验证方法研究
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-8页 |
| 图表清单 | 第8-11页 |
| 注释表 | 第11-12页 |
| 第一章 绪论 | 第12-17页 |
| ·课题研究背景 | 第12-13页 |
| ·国内外研究现状及选题依据 | 第13-15页 |
| ·国内外研究现状 | 第13-15页 |
| ·选题依据 | 第15页 |
| ·论文的组织结构 | 第15-17页 |
| 第二章 传统故障树分析法和模型检验 | 第17-27页 |
| ·传统故障树分析法（FTA） | 第17-22页 |
| ·故障树的构建过程 | 第18-21页 |
| ·故障树的定性分析 | 第21-22页 |
| ·模型检验 | 第22-24页 |
| ·模型检验的过程 | 第23-24页 |
| ·主流的模型检验技术 | 第24页 |
| ·FTA 与模型检验的结合 | 第24-26页 |
| ·传统故障树的适用范围 | 第24-25页 |
| ·模型检验技术的特点分析 | 第25页 |
| ·基于 FTA 的模型检验方法 | 第25-26页 |
| ·本章小结 | 第26-27页 |
| 第三章 线性时序故障树（LTFT）的构建及约简 | 第27-41页 |
| ·用线性时序逻辑形式化规约的 LTFT | 第27-32页 |
| ·线性时序逻辑 | 第27-29页 |
| ·LTFT 的构建 | 第29-32页 |
| ·LTFT 约简 | 第32-40页 |
| ·FAUNET 约简规则 | 第32-35页 |
| ·支持安全属性验证的 LTFT 约简流程 | 第35-40页 |
| ·本章小结 | 第40-41页 |
| 第四章 LTFT 安全属性提取及验证 | 第41-59页 |
| ·LTFT 安全属性提取 | 第41-48页 |
| ·LTFT 的形式化存储 | 第41-42页 |
| ·安全属性提取算法 | 第42-48页 |
| ·软件系统形式化建模 | 第48-53页 |
| ·Promela 建模机制 | 第48-50页 |
| ·软件系统的 Promela 抽象建模 | 第50-53页 |
| ·软件模型安全属性验证 | 第53-58页 |
| ·当前主流验证工具的分析 | 第53-55页 |
| ·安全属性的 Espin 验证 | 第55-58页 |
| ·本章小结 | 第58-59页 |
| 第五章 航电软件系统实例研究 | 第59-76页 |
| ·软件系统故障树构建 | 第59-61页 |
| ·襟缝翼控制系统简介 | 第59-60页 |
| ·襟缝翼控制系统故障树建模 | 第60-61页 |
| ·软件系统 LTFT 构建及约简 | 第61-68页 |
| ·襟缝翼控制系统 LTFT 模块化构建 | 第62-65页 |
| ·襟缝翼控制系统 LTFT 约简 | 第65-68页 |
| ·软件系统安全属性提取与验证 | 第68-75页 |
| ·襟缝翼控制系统安全属性提取 | 第68-69页 |
| ·襟缝翼控制系统安全性验证与分析 | 第69-75页 |
| ·本章小结 | 第75-76页 |
| 第六章 总结与展望 | 第76-78页 |
| ·论文总结 | 第76页 |
| ·未来工作展望 | 第76-78页 |
| 参考文献 | 第78-83页 |
| 致谢 | 第83-85页 |
| 在学期间的研究成果及发表的学术论文 | 第85-86页 |
| 附录 | 第86-87页 |
