嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为当前的研究热点。故障树能够自底向上地描述软件失效发生的因果关系链，可以通过故障树分析，从中提取出系统安全属性，但是却无法验证系统本身是否满足这些安全属性。而且由于其非形式化方法的局限性，传统的故障树也无法精确描述安全关键系统中具有时序特征的系统故障。计算机领域的模型检验技术能够对待验证系统的相关性质进行精确地验证，并准确定位错误执行轨迹，但在待验证性质的提取方面仍存在着技术瓶颈。本文结合传统故障树分析的系统性与模型检验形式化表达的精确性等优点，提出一种基于故障树分析的软件安全性验证方法。首先，对传统故障树进行扩充，并结合形式化方法提出一种用线性时序逻辑规约的能够描述软件系统时序故障的线性时序故障树——LTFT，并根据安全性验证的需求给出一套支持安全属性验证的LTFT约简规则。然后，利用LTFT的特点改进了传统故障树的割集分析算法，提出一个基于LTFT割集分析的安全属性提取算法，并运用该算法提取出LTFT所描述的软件系统安全属性。再针对安全属性对软件系统抽象建模并对软件模型进行验证，判断该安全属性在软件的设计中是否得到满足，为软件安全性验证提供有效证据。最后，通过对工程实践中的一个飞机襟缝翼控制系统进行故障树建模和安全属性提取，并用本文自行开发的一款基于SPIN的图形化软件模型检验工具——Espin对其进行安全性验证，对验证结果进行分析，最终说明了文章方法的可行性和有效性。