传统的演绎式安全性分析由安全性工程师通过手动实施，采用的分析方法主要有故障树分析等，但是这些分析方法都存在一些弊端：高度主观并且依赖分析人员的技能和经验，而且不太可能做到完整无错。如果能将这些时间和精力用于建立所研究系统的模型并对故障模型进行分析，或许能减少通过手动实施所需的耗费并且提高分析的质量。形式化验证技术，如模型检验方法，能够很好地处理复杂度较高的系统，并且能在一定程度上克服这些弊端。本文分析总结了目前通用的飞机系统安全评估流程及常用的演绎式安全性分析方法，并以故障树分析、可靠性框图等方法为例介绍了分析流程，指出了演绎式安全性分析方法中存在的局限性。为此，通过对形式化模型检验方法的研究，将其引入飞机系统安全分析领域，提出了基于形式化模型检验的飞机系统演绎式安全分析方法，并给出了具体的分析流程。针对模型检验工具输出的可达状态结果集开发了后处理分析平台，对可达状态集进行后续处理分析处理。最后以飞机第二动力系统为案例研究对象，实施了基于形式化模型检验的演绎式安全性分析，得到故障树、最小割集等定性分析结果。