| 摘要 | 第4-6页 |
| Abstract | 第6-7页 |
| 缩略词 | 第13-14页 |
| 第一章 绪论 | 第14-25页 |
| 1.1 研究背景 | 第14-17页 |
| 1.1.1 软件安全性分析 | 第14-16页 |
| 1.1.2 嵌入式软件系统的构件化特征 | 第16页 |
| 1.1.3 构件化嵌入式软件安全性分析面临的挑战 | 第16-17页 |
| 1.2 国内外研究现状 | 第17-22页 |
| 1.2.1 安全性分析模型 | 第17-20页 |
| 1.2.2 安全性分析工具 | 第20-21页 |
| 1.2.3 现有方法存在的问题 | 第21-22页 |
| 1.3 研究内容 | 第22-23页 |
| 1.4 论文结构安排 | 第23-25页 |
| 第二章 基于形式化方法的软件安全性分析基础 | 第25-35页 |
| 2.1 软件安全性及相关概念定义 | 第25-26页 |
| 2.2 基于形式化方法的软件安全性分析框架 | 第26-27页 |
| 2.3 软件安全性设计模型 | 第27-31页 |
| 2.3.1 软件静态结构的安全性设计模型 | 第28-29页 |
| 2.3.2 软件动态失效行为的安全性设计模型 | 第29-31页 |
| 2.4 软件形式化分析模型 | 第31-34页 |
| 2.4.1 块依赖图 | 第31-32页 |
| 2.4.2 接口自动机 | 第32-33页 |
| 2.4.3 交互马尔可夫链 | 第33-34页 |
| 2.5 本章小结 | 第34-35页 |
| 第三章 构件化嵌入式软件静态结构的安全性分析 | 第35-46页 |
| 3.1 软件静态结构安全性分析问题提出 | 第35-36页 |
| 3.2 软件构件安全等级依赖目标分析 | 第36-38页 |
| 3.3 基于Sys ML块定义图的安全性设计模型的建立 | 第38-40页 |
| 3.3.1 SysML块定义图 | 第38-39页 |
| 3.3.2 带安全等级信息的SysML块定义图的建立 | 第39-40页 |
| 3.4 嵌入式软件构件安全等级依赖分析 | 第40-45页 |
| 3.4.1 SysML块定义图的形式化表示 | 第41-42页 |
| 3.4.2 安全性依赖的一致性分析 | 第42-45页 |
| 3.5 相关工作比较 | 第45-46页 |
| 3.6 本章小结 | 第46页 |
| 第四章 基于接口自动机的软件失效行为安全性分析 | 第46-60页 |
| 4.1 软件失效行为安全性分析的问题提出 | 第47-48页 |
| 4.2 状态事件故障树的建立 | 第48-49页 |
| 4.3 卫式接口自动机(GIA)的提出 | 第49-53页 |
| 4.3.1 GIA模型 | 第49-51页 |
| 4.3.2 GIA弱互模拟 | 第51-53页 |
| 4.4 基于GIA的SEFT构件与逻辑门的语义 | 第53-56页 |
| 4.4.1 SEFT构件的GIA语义 | 第53页 |
| 4.4.2 SEFT逻辑门的GIA语义 | 第53-56页 |
| 4.5 SEFT的形式语义以及最小割序集分析 | 第56-59页 |
| 4.5.1 SEFT的GIA语义生成 | 第56-57页 |
| 4.5.2 GIA弱互模拟等价类划分及SEFT最小割序集分析 | 第57-59页 |
| 4.6 相关工作比较 | 第59页 |
| 4.7 本章小结 | 第59-60页 |
| 第五章 基于交互马尔可夫链的软件失效行为安全性参数分析 | 第60-77页 |
| 5.1 软件失效行为安全性参数分析的问题提出 | 第60-61页 |
| 5.2 接口交互马尔可夫链(Interface-IMC)的建立 | 第61-66页 |
| 5.2.1 Interface-IMC模型 | 第61-62页 |
| 5.2.2 Interface-IMC的并行组合 | 第62-63页 |
| 5.2.3 Interface-IMC的状态等价 | 第63-66页 |
| 5.3 基于Interface-IMC的SEFT构件和逻辑门形式化描述 | 第66-68页 |
| 5.3.1 SEFT构件的Interface-IMC语义 | 第66-67页 |
| 5.3.2 SEFT逻辑门的Interface-IMC语义 | 第67-68页 |
| 5.4 SEFT的Interface-IMC语义生成 | 第68-72页 |
| 5.4.1 Interface-IMC的并行组合 | 第69-70页 |
| 5.4.2 Interface-IMC弱互模拟等价类划分方法 | 第70-72页 |
| 5.5 SEFT的概率以及时间参数的分析方法 | 第72-75页 |
| 5.5.1 SEFT的概率特性计算 | 第72-74页 |
| 5.5.2 SEFT的时间特性计算 | 第74-75页 |
| 5.6 相关工作比较 | 第75-76页 |
| 5.7 本章小结 | 第76-77页 |
| 第六章 工具设计和案例分析 | 第77-92页 |
| 6.1 软件安全性分析工具的设计 | 第77-80页 |
| 6.1.1 相关安全性分析工具的分析 | 第77-78页 |
| 6.1.2 工具的系统结构 | 第78-80页 |
| 6.2 相关案例分析 | 第80-91页 |
| 6.2.1 系统静态结构安全性依赖实例 | 第80-83页 |
| 6.2.2 软件失效行为的安全性分析实例 | 第83-85页 |
| 6.2.3 软件失效行为的安全性参数分析实例 | 第85-91页 |
| 6.3 本章小结 | 第91-92页 |
| 第七章 结束语 | 第92-95页 |
| 7.1 本文的主要工作 | 第92-93页 |
| 7.2 进一步的研究工作 | 第93-95页 |
| 参考文献 | 第95-105页 |
| 致谢 | 第105-106页 |
| 在学期间的研究成果及发表的学术论文 | 第106-107页 |
