FTA(故障树分析)是系统可靠性和安全性分析的一种简单、有效的方法。它最初是由美国贝尔实验室在研究电话拨号机的自动控制系统可靠性时提出的,至今已有50年历史,在安全关键领域发挥了巨大作用。20世纪80年代,软件的可靠性和安全性开始成为科技界关注的课题,为了适应软件安全性分析的需要,传统上用于硬件可靠性、安全性分析的故障树分析法被移植到软件这个新领域,并得到了进一步的扩充。随着软件在各类系统中的应用,系统故障的描述也越来越复杂,难以用现有故障树进行描述,于是人们根据需要引入了一些新的逻辑门,产生了动态故障树和时序故障树。现有时序故障树语义的形式化逻辑虽然简明,易于理解掌握,但表达能力有限,且缺乏工具的支持。同时,现有模型检验技术以其成熟性和自动化程度高等优点颇受人们青睐,但其存在着待验证性质难以提取的问题。如何找到一种适合时序故障树语义描述,并且有现成工具支持的逻辑语言对时序故障树语义进行形式化,是时序故障树分析与模型检验方法相结合的重点。故障树的构建和分析是相当繁琐费时的,非常容易出错,如何在使用中方便地对系统故障树进行构建和分析,并对所建故障树的正确性进行有效的检测,是故障树应用中需要解决的难题。针对以上存在的问题及需求,本文基于TCTL对现有时序故障树进行扩充,使之能够表达更加复杂的故障和系统规约。采用TCTL对时序故障树的语义进行形式化,通过故障树分析技术提取顶层事件的形式化规约,以TCTL的形式进行表示,便于被现有模型检验工具UPPAAL验证。根据软件相关系统的特点,提出了一种基于测试的故障树正确性检测方法,该方法能够有效检测出故障树构建中易犯的多种错误。同时,基于Eclipse的图形编辑框架GEF和富客户端平台RCP,采用JAVA语言开发了时序故障树分析软件,实现了时序故障树辅助生成及自动化分析功能,且能够提取目标事件的形式化规约。