增强飞行视景系统作为飞机上的复杂电子系统,传统的安全性分析面临工作量大,过于依赖分析人员经验,容易出错等问题,Petri网、概率模型等形式化方法虽然提高了分析的自动化水平,减少了一定的分析工作量,但也面临不能自上而下进行安全性需求分配的问题。为解决上述问题,提出了基于模型检验的形式化安全性分析方法。实现对增强飞行视景系统的定性、定量安全性分析,提高分析效率。研究包括以下几个方面:(1)首先,通过对该系统的架构和数据流进行抽象,分模块级、LRU级、系统级三层,建立了系统的形式化名义模型,并进行了验证。(2)研究模型扩展方法,编写故障库模板,将底层模块的故障模式注入到名义模型,建立形式化扩展模型。(3)将典型失效状态用形式化规约描述,进行自动计算,得到故障树最小割集,基于该最小割集进行了定性和定量分析,其中在定量分析,提出一种安全性分配方法,并实现了自动分配工具。结果表明,该方法自动化程度高,且解决了其它形式化方法如Petri网、概率模型等无法进行自上而下概率分配的问题,能够更加有效地促进系统设计阶段的安全性工作。