| 摘要 | 第4-5页 |
| abstract | 第5-6页 |
| 第一章 绪论 | 第14-23页 |
| 1.1 研究背景 | 第14-17页 |
| 1.2 研究现状 | 第17-20页 |
| 1.3 研究意义 | 第20页 |
| 1.4 论文的研究内容 | 第20-21页 |
| 1.5 论文组织结构 | 第21-23页 |
| 第二章 背景知识 | 第23-33页 |
| 2.1 现代民机中的航电系统设计的安全性要求 | 第23-26页 |
| 2.1.1 适航的概念 | 第23-25页 |
| 2.1.2 ARP4754 | 第25页 |
| 2.1.3 ARP4761 | 第25-26页 |
| 2.2 基于模型的系统安全性分析方法 | 第26-28页 |
| 2.3 MBSA过程中的关键技术 | 第28-32页 |
| 2.3.1 RSML~(-e)规范语言 | 第28页 |
| 2.3.2 NuSMV模型检验系统 | 第28-29页 |
| 2.3.3 故障树分析 | 第29-31页 |
| 2.3.4 失效模式与影响分析 | 第31-32页 |
| 2.4 本章小结 | 第32-33页 |
| 第三章 面向系统需求的形式化建模与验证方法 | 第33-50页 |
| 3.1 RSML~(-e)与四变量模型 | 第33-38页 |
| 3.1.1 四变量模型概述 | 第33-34页 |
| 3.1.2 RSML~(-e)语义概述 | 第34-38页 |
| 3.2 NuSMV模型检验语言 | 第38-43页 |
| 3.2.1 模型检验 | 第38-40页 |
| 3.2.2 NuSMV语言 | 第40-43页 |
| 3.3 RSML~(-e)到NuSMV语言的转化规则 | 第43-48页 |
| 3.4 基于NuSMV的初步需求验证框架 | 第48-49页 |
| 3.5 本章小结 | 第49-50页 |
| 第四章 基于MBSA的故障扩展与分析 | 第50-62页 |
| 4.1 方法概述 | 第50-51页 |
| 4.2 故障扩展 | 第51-57页 |
| 4.2.1 故障注入机制 | 第51-52页 |
| 4.2.2 故障模式与模型扩展机制 | 第52-54页 |
| 4.2.3 故障扩展指令语言 | 第54-57页 |
| 4.3 基于模型检验的系统验证与安全分析 | 第57-60页 |
| 4.3.1 验证系统性质 | 第57-58页 |
| 4.3.2 故障树生成 | 第58-59页 |
| 4.3.3 FMEA表的生成 | 第59-60页 |
| 4.4 xSAP－基于模型检验的系统安全分析平台 | 第60-61页 |
| 4.5 基于MBSA的系统验证与安全性分析框架 | 第61页 |
| 4.6 本章小结 | 第61-62页 |
| 第五章 自动飞行系统的形式化建模 | 第62-80页 |
| 5.1 实例系统架构概述 | 第62-70页 |
| 5.1.1 GarminG1000系统概述 | 第62-63页 |
| 5.1.2 AFCS简介 | 第63-64页 |
| 5.1.3 飞行导引系统简介 | 第64-66页 |
| 5.1.4 FGS功能需求 | 第66-67页 |
| 5.1.5 FGS模式 | 第67-68页 |
| 5.1.6 FGS模式逻辑模型 | 第68-70页 |
| 5.2 构建AFCS系统的RSML~(-e)模型 | 第70-76页 |
| 5.2.1 第一层模型的RSML~(-e)建模 | 第71-74页 |
| 5.2.2 飞行指引仪的RSML~(-e)模型 | 第74-75页 |
| 5.2.3 垂直速度模式的RSML~(-e)模型 | 第75-76页 |
| 5.3 将AFCS系统的RSML~(-e)模型转化为NuSMV模型 | 第76-79页 |
| 5.4 本章小节 | 第79-80页 |
| 第六章 基于模型的自动飞行系统的安全性分析与验证 | 第80-94页 |
| 6.1 验证NUSMV功能模型 | 第80-85页 |
| 6.1.1 转换安全属性到NuSMV语句 | 第80-81页 |
| 6.1.2 NuSMV安全属性验证 | 第81-85页 |
| 6.2 对AFCS系统的NuSMV模型进行故障扩展 | 第85-88页 |
| 6.2.1 故障注入 | 第85-86页 |
| 6.2.2 自定义故障模式 | 第86-87页 |
| 6.2.3 故障扩展 | 第87-88页 |
| 6.3 安全评估 | 第88-93页 |
| 6.3.1 验证系统性质 | 第88-89页 |
| 6.3.2 生成故障树 | 第89-92页 |
| 6.3.3 生成FMEA表 | 第92-93页 |
| 6.4 本章小结 | 第93-94页 |
| 第七章 总结与展望 | 第94-96页 |
| 7.1 研究总结 | 第94-95页 |
| 7.2 未来工作展望 | 第95-96页 |
| 参考文献 | 第96-102页 |
| 致谢 | 第102-103页 |
| 在学期间的研究成果及发表的学术论文 | 第103页 |
