随着机载软件的功能愈加强大,其复杂性也随之提高,软件失效逐渐成为了引发系统失效的重要因素之一,如何保证机载软件安全性已成为研究重点。随着模型技术的应用,越来越多的软件采用构件化的软件设计方法来开发机载软件,常规的软件安全性分析方法难以分析构件化软件的内部失效行为,而状态事件故障树模型组合了构件故障树和基于状态的建模技术,适合用来开展构件化软件的安全性分析工作,分析并获取安全性规约。为了提高软件的安全性,在安全性分析工作的基础上,可以开展形式化验证工作,检测并消除软件中可能存在的危险行为。为此,本文提出了一种基于状态事件故障树的软件形式化验证方法,并开展了适航目标符合性验证工作,给出了软件满足的适航目标及其相关的符合性证据,为机载软件的适航目标符合性验证提供了一个实施方案。本文的主要研究工作如下:（1）针对机载软件的安全性需求分析问题,以固定翼无人机飞控软件为研究对象,提出一种基于状态事件故障树的构件化软件安全性规约获取方法,该方法从系统结构和软件功能出发,建立状态事件故障树模型。然后定义了逻辑门转换规则和构件排序规则,将状态事件故障树转换为顺序二元决策图模型,分析得到最小割序集并获取软件安全性规约,完成对飞控软件的安全性分析。（2）针对机载软件设计模型的形式化验证问题,采用模型检测的形式化方法对软件进行验证,基于飞控软件功能给出软件设计模型,然后将安全性规约和软件模型作为输入开展模型检测工作,检测并消除软件中潜在的危险行为,完成对软件的形式化验证。（3）针对机载软件的适航目标符合性验证问题,识别出了形式化分析过程在软件需求过程和软件设计过程中需要满足的适航目标,然后给出了需开展的验证活动,最后基于形式化模型和模型检测结果,给出了这些目标的符合性程度及符合性证据说明。本文提出的方法以固定翼无人机飞控软件为研究对象,给出了构建软件状态事件故障树及分析获取安全性规约的过程,并对软件的形式化模型进行验证和分析,检测并消除了软件中存在的危险路径,说明了本文方法的有效性,为提高构件化机载软件的安全性提供了一种新方法。