随着计算机软件在安全关键领域的广泛应用，人们对软件安全性可靠性的要求越来越高。为了提高软件质量，针对软件模型的安全性分析方法一直是学术研究的热点问题。传统的状态图分析法能够通过对组件行为的分析，判断其设计是否满足功能需求，但不能针对故障问题进行有效分析，安全属性的提取一直依靠经验完成。故障树虽然能够充分描述造成软件失效的因素和因素间的关系，却无法确定这种故障是否在系统中真实存在。本文通过对故障树和状态图分析法的深入研究，提出了故障扩展状态图的概念，并结合当前热门的模型检测技术，将其用于软件的安全性分析工作。本文的主要研究内容包括：1．综合故障树和状态图分析法的优势，提出故障扩展状态图的概念，统一了系统的安全需求模型与功能模型，分析了利用其进行软件安全性分析的可行性；2．通过对故障树的半形式化描述，提取其故障信息，并利用故障树逻辑门的转换规则和故障元素的语义映射，扩展系统原始状态图，给出了构造故障扩展状态图的方法；3．根据故障扩展状态图的性质，将系统的安全性需求转化为故障状态的可达性，结合模型检测技术，提出了基于故障扩展状态图的系统形式化建模和安全性验证的方法；4．运用本文提出的方法，对一个小型微波炉系统进行案例分析，在我们开发的模型检测环境ESpin下，通过安全属性的提取、故障扩展状态图的建立和故障状态可达性的验证，定位系统模型中的错误并给出解决方案，证明了本文方法的可行性和有效性。