航电系统作为飞机的核心系统之一,是一种典型的安全关键系统。先进的综合模块化航电系统在提高资源利用率和运行效率的同时,给系统安全性工作带来了更大的挑战。故障树分析是提高系统安全性和可靠性的有效方法。但传统的人工生成故障树的方式使得故障树分析的质量取决于工程师的个人技巧同时容易出错,并且难以处理大型系统的高复杂度。基于模型的安全性分析技术以拥有严格语义的形式化模型为基础,通过模型检测等自动化分析技术提高了安全性分析的准确性与分析效率。然而现有的安全性分析工作通常都面临着故障空间过大的困难。本文以综合航系统电安全性分析为背景,针对传统安全性分析技术难以分析复杂系统交互的问题,从基于模型的安全性分析思路出发,开展了如何利用模型检测自动生成系统故障树的研究。具体研究内容如下所述:本文将软件产品线领域常用的特征模型引入安全性分析过程,利用特征模型描述不同的系统配置。首先,通过从系统环境、组件(功能)及组件故障等不同层次提取系统特征及特征间的约束关系,本文建立了系统特征模型从而清晰地描述了安全工程师的领域知识,缩小了故障空间。然后,在系统特征模型的基础上,提出了一种结合系统特征建模与行为建模的基于模型检测的故障树自动生成框架。该框架以系统特征模型与行为模型为基础,利用模型检测技术同时对多种配置下的系统行为进行分析,提高了安全性分析的效率。在系统行为建模方面,通过对Kripke结构的拓展,本文提出了故障标记迁移系统,将系统特征与系统及故障行为联系起来,从而对不同配置下的系统行为进行建模与分析。然后将故障树自动生成问题转化为故障标记迁移系统上的模型检测问题。在证明了故障标记迁移系统与特征迁移系统表达能力等价的基础上,本文通过修改现有模型检测工具SNIP的算法实现了所提出的故障树生成方案。基于所提出的故障树自动生成方法,我们以修改后的SNIP模型检测器为核心设计并实现了故障树自动生成工具。该工具拥有特征模型图形化展示,故障树生成与图形展示等功能。最后,本文以A320飞机液压系统为实例进行了实验分析,验证了所提出的基于模型检测的故障树生成方法的有效性。