传统的安全性分析方法，受到分析人员自身技能和经验等因素的影响，一定程度上存在容易疏漏系统失效状态或误判失效影响的局限性，因此有必要在飞机系统安全分析领域中引入新方法。模型检验方法使用了计算机技术，通过验证工具列出模型系统的所有状态，并能按照逻辑表达式的描述对全部状态进行搜索，在得到安全性分析结果的同时能够降低对分析人员能力的要求。本文研究了模型检验理论、计算机实现原理和验证工具，分析总结了目前通用的飞机系统安全性评估流程和安全性分析方法，剖析了故障树分析方法流程，指出了其存在的局限性。为此，本文将模型检验方法应用到飞机系统安全性分析中。以系统需求规范为分析起点，给出了一种基于模型检验的飞机系统安全性分析流程。根据前述工作，本文开发了基于NuSMV安全验证平台，平台使用了数据库技术，建立了基本的元件代码库和失效代码库，可以帮助用户快速构建系统模型、生成验证代码和知识库文件。最后以ARP4761附录中的机轮刹车系统为例，使用模型检验方法对其安全性进行了分析。