学位论文 > 优秀研究生学位论文题录展示
软件时序故障树建模与分析技术研究
作 者: 刘磊
导 师: 齐治昌;董威
学 校: 国防科学技术大学
专 业: 计算机科学与技术
关键词: FTA 时序故障树 GEF 性质提取 自动化分析
分类号: TP311.52
类 型: 硕士论文
年 份: 2011年
下 载: 31次
引 用: 0次
阅 读: 论文下载
内容摘要
FTA(故障树分析)是系统可靠性和安全性分析的一种简单、有效的方法。它最初是由美国贝尔实验室在研究电话拨号机的自动控制系统可靠性时提出的,至今已有50年历史,在安全关键领域发挥了巨大作用。20世纪80年代,软件的可靠性和安全性开始成为科技界关注的课题,为了适应软件安全性分析的需要,传统上用于硬件可靠性、安全性分析的故障树分析法被移植到软件这个新领域,并得到了进一步的扩充。随着软件在各类系统中的应用,系统故障的描述也越来越复杂,难以用现有故障树进行描述,于是人们根据需要引入了一些新的逻辑门,产生了动态故障树和时序故障树。现有时序故障树语义的形式化逻辑虽然简明,易于理解掌握,但表达能力有限,且缺乏工具的支持。同时,现有模型检验技术以其成熟性和自动化程度高等优点颇受人们青睐,但其存在着待验证性质难以提取的问题。如何找到一种适合时序故障树语义描述,并且有现成工具支持的逻辑语言对时序故障树语义进行形式化,是时序故障树分析与模型检验方法相结合的重点。故障树的构建和分析是相当繁琐费时的,非常容易出错,如何在使用中方便地对系统故障树进行构建和分析,并对所建故障树的正确性进行有效的检测,是故障树应用中需要解决的难题。针对以上存在的问题及需求,本文基于TCTL对现有时序故障树进行扩充,使之能够表达更加复杂的故障和系统规约。采用TCTL对时序故障树的语义进行形式化,通过故障树分析技术提取顶层事件的形式化规约,以TCTL的形式进行表示,便于被现有模型检验工具UPPAAL验证。根据软件相关系统的特点,提出了一种基于测试的故障树正确性检测方法,该方法能够有效检测出故障树构建中易犯的多种错误。同时,基于Eclipse的图形编辑框架GEF和富客户端平台RCP,采用JAVA语言开发了时序故障树分析软件,实现了时序故障树辅助生成及自动化分析功能,且能够提取目标事件的形式化规约。
|
全文目录
摘要 8-9 ABSTRACT 9-10 第一章 绪论 10-20 1.1 课题研究背景 10-11 1.2 国内外研究现状 11-17 1.2.1 故障树理论研究 11-12 1.2.2 故障树应用 12-13 1.2.3 故障树计算机辅助生成和分析 13-17 1.3 论文的主要工作及创新 17-18 1.4 论文的组织结构 18-20 第二章 故障树分析法 20-44 2.1 引言 20-26 2.1.1 FTA 的应用范围和特点 20-21 2.1.2 FTA 的主要步骤 21-22 2.1.3 FTA 存在的主要问题 22-23 2.1.4 FTA 中的名词术语和符号 23-26 2.2 故障树的构造 26-30 2.3 故障树分析的主要内容 30-43 2.3.1 单调关联故障树 30-31 2.3.2 定性分析 31-35 2.3.3 故障树主要参数间的相互转换 35-39 2.3.4 定量分析 39-43 2.4 小结 43-44 第三章 基于时序故障树的软件规约与验证 44-61 3.1 时序逻辑 44-48 3.1.1 CTL(Computation Tree Logic) 45-46 3.1.2 TCTL(Timed Computation Tree Logic) 46-48 3.2 时序故障树建模 48-52 3.2.1 现有时序故障树建模 48-51 3.2.2 基于TCTL 扩充后的时序故障树模型 51-52 3.3 时序故障树的定性分析及其验证 52-58 3.3.1 时序故障树定性分析方法 53-56 3.3.2 顶层事件规约的提取验证 56-58 3.4 实例分析 58-60 3.5 小结 60-61 第四章 时序故障树的正确性检测 61-76 4.1 时序故障树形式化 61-63 4.1.1 时序故障树的形式化定义 61-63 4.1.2 时序故障树语义的形式化 63 4.2 故障树正确性检测 63-71 4.2.1 方法框架 65-67 4.2.2 测试用例的生成 67-71 4.3 实例 71-75 4.4 小结 75-76 第五章 时序故障树自动化分析工具的设计与实现 76-93 5.1 现有计算机辅助建树法及其特点 76-77 5.2 GEF 介绍 77-80 5.2.1 GEF 架构概述 78-79 5.2.2 GEF 工作原理 79-80 5.3 设计目标及框架 80-81 5.4 节点类的设计 81-82 5.5 主要功能的实现方法 82-90 5.5.1 基础框架的实现 83-85 5.5.2 故障树构建功能的实现 85-88 5.5.3 求解最小割集的实现 88-90 5.5.4 提取形式化规约功能的实现 90 5.6 实例分析 90-92 5.7 小结 92-93 第六章 总结与展望 93-94 致谢 94-95 参考文献 95-100 作者在学期间取得的学术成果 100
|
相似论文
- 水利枢纽机电设备维修管理模式研究,TH17
- 机载语音通信系统适航安全性研究,TN919.8
- FMEA与FTA在阴极电泳项目质量管理中的应用研究,F426.6
- 基于危害性分析的数控机床主传动系统可靠性分析,TG659
- 参与式社区共管地区农户生计结构研究,C924.21
- 日本FTA/EPA谈判中农产品贸易自由化策略分析,F753.13
- FTA背景下的中日韩农产品贸易研究,F752.7
- 中国—挪威建立FTA的经济效应研究,F752.7
- 中国—澳大利亚建立FTA的经济效应研究,F752
- 基于HAZOP的往复压缩机组安全评价指标体系的建立,TE974
- GEF图形编辑器自动生成的研究,TP391.41
- 中美自由贸易的基础与障碍,F752.7
- 语境顺应视角下模糊限制语语用功能分析,H030
- 中韩FTA建立中的农业问题,F752.7
- 韩美FTA谈判及对中韩FTA的影响,F752.7
- 建立韩中FTA对韩中电子产品贸易效果的实证分析,F752.7
- 建筑施工安全评价的研究,X947
- BPEL图形化服务组合工具的设计与实现,TP311.52
- FMEA与FTA在汽车覆盖件模具项目质量管理中的应用研究,F273.2
- 基于BPEL的服务生成系统的研究与实现,TP393.09
中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 软件工程 > 软件开发
© 2012 www.xueweilunwen.com
|