软件时序故障树建模与分析技术研究

论文摘要

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

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 课题研究背景
• 1.2 国内外研究现状
• 1.2.1 故障树理论研究
• 1.2.2 故障树应用
• 1.2.3 故障树计算机辅助生成和分析
• 1.3 论文的主要工作及创新
• 1.4 论文的组织结构
• 第二章 故障树分析法
• 2.1 引言
• 2.1.1 FTA 的应用范围和特点
• 2.1.2 FTA 的主要步骤
• 2.1.3 FTA 存在的主要问题
• 2.1.4 FTA 中的名词术语和符号
• 2.2 故障树的构造
• 2.3 故障树分析的主要内容
• 2.3.1 单调关联故障树
• 2.3.2 定性分析
• 2.3.3 故障树主要参数间的相互转换
• 2.3.4 定量分析
• 2.4 小结
• 第三章 基于时序故障树的软件规约与验证
• 3.1 时序逻辑
• 3.1.1 CTL（Computation Tree Logic）
• 3.1.2 TCTL（Timed Computation Tree Logic）
• 3.2 时序故障树建模
• 3.2.1 现有时序故障树建模
• 3.2.2 基于TCTL 扩充后的时序故障树模型
• 3.3 时序故障树的定性分析及其验证
• 3.3.1 时序故障树定性分析方法
• 3.3.2 顶层事件规约的提取验证
• 3.4 实例分析
• 3.5 小结
• 第四章 时序故障树的正确性检测
• 4.1 时序故障树形式化
• 4.1.1 时序故障树的形式化定义
• 4.1.2 时序故障树语义的形式化
• 4.2 故障树正确性检测
• 4.2.1 方法框架
• 4.2.2 测试用例的生成
• 4.3 实例
• 4.4 小结
• 第五章 时序故障树自动化分析工具的设计与实现
• 5.1 现有计算机辅助建树法及其特点
• 5.2 GEF 介绍
• 5.2.1 GEF 架构概述
• 5.2.2 GEF 工作原理
• 5.3 设计目标及框架
• 5.4 节点类的设计
• 5.5 主要功能的实现方法
• 5.5.1 基础框架的实现
• 5.5.2 故障树构建功能的实现
• 5.5.3 求解最小割集的实现
• 5.5.4 提取形式化规约功能的实现
• 5.6 实例分析
• 5.7 小结
• 第六章 总结与展望
• 致谢
• 参考文献
• 作者在学期间取得的学术成果