基于故障配置的故障树生成

发布时间：2022-01-13 10:07

　　故障树分析是提高系统安全性和可靠性的有效方法。传统的人工故障树生成方式难以解决当前系统的庞大规模与复杂性的问题,且容易出错。为此,提出基于故障配置的故障树生成方法,引入软件产品线的可变性管理,用于系统故障建模与形式化分析。首先,定义故障特征图模型用于刻画系统故障间的约束关系,基于Kripke结构定义故障标记迁移系统来描述系统的行为;然后,基于模型的语义建立通过模型检测生成故障树的过程;最后,通过时序逻辑描述系统安全属性,利用模型检测工具SNIP验证安全属性进而生成故障树。案例研究验证了该方法的有效性。 

【文章来源】：计算机科学. 2017,44(02)北大核心CSCD

【文章页数】：10 页

【部分图文】：

图１数据采集器系统

偏离故障，则数据值每次增加２，且不再进行重置。该故障为瞬时性故障（ＴｒａｎｓｉｅｎｔＦａｕｌｔ），即组件发生故障后可能会恢复正常。２）传感器单元也可能发生固定型故障。当传感器发生瘫痪后，采集到的数据值会保持为一个固定的值不再发生变化。该故障一旦发生，其影响是永久性的（ＰｅｒｍａｎｅｎｔＦａｕｌｔ），组件无法再恢复正常。３）过滤器单元可能发生与传感器单元类似的固定型故障，过滤器单元的数据保持为固定数值而不再变化，该故障属于永久性故障。数据采集器系统的故障特征图如图３所示。故障特征图是一种树状图，图中的每一个节点表示一个故障特征，其中根节点表示数据采集器系统的故障；叶节点表示系统元件的基本故障；中间节点表示系统模块的故障。故障特征图中的边刻画了故障特征间的约束关系，图３示例表示的是与关系、或关系等。图３中，特征Ｓ１和Ｓ２以与关系连接到特征ＳＳ，表示传感器模块的故障包括优先和备份传感器单元的故障；特征Ｓ１ＤＴ和Ｓ１ＳＰ表示优先传感器可能发生的故障，二者均标记为可选且以与关系连接，表示在系统运行过程中二者互不影响，从而可能出现３种情况，即二者都发生、其中之一发生或都不发生；特征Ｓ２ＤＴ和Ｓ２ＳＰ也为可选故障，但与前面不同的是二者以异或关系连接到特征Ｓ２，表示在系统的一次运行过程中，备份传感器单元的这两种故障不会同时出现。图３数据采集器系统故障特征图现有的安全性分析技术在对故障建模时通常只是描述其起源、传播或具体行为，而没有对故障间的约束关系进行刻１８４计算机科学２０１７年

配置（ＦａｕｌｔＣｏｎｆｉｇｕｒａｔｉｏｎ）。故障特征图的语义即所有合法的系统故障配置的集合记作［［ｆｆｄ］］ＦＦＤ，且［［ｆｆｄ］］ＦＦＤ?｛２Ｆ｝。以数据采集器系统为例，如图３所示，根据故障特征图的语法，数据采集器系统的故障特征集合为Ｆａｕｌｔ＝｛Ｓ１ＳＰ，Ｓ１ＤＴ，Ｓ２ＳＰ，Ｓ２ＤＴ，Ｆ１ＳＰ，Ｆ２ＳＰ｝，而系统所有的故障配置集合为｛２Ｆａｕｌｔ｝。３．２故障标记迁移系统传统的模型检测过程通常采用状态迁移系统对系统行为进行建模。Ｋｒｉｐｋｅ结构［２１］是一种常用的系统模型，包含系统状态和系统状态迁移关系。为了对包含故障特征的系统行为进行分析，本文对Ｋｒｉｐｋｅ结构进行拓展并提出故障标记迁移系统（ＦａｕｌｔＬａｂｅｌｅｄＴｒａｎｓｉｔｉｏｎＳｙｓｔｅｍ，ＦＬＴＳ），通过在迁移关系上添加特征标记来区分迁移关系描述的行为。故障标记迁移系统的形式化定义如下。定义５一个ＦＬＴＳ是一个元组ｆｌｔｓ＝（Ｓ，Ｉ，Ｐ，Ｒ，Ｌ，ｆｆｄ，γ），其中：Ｓ是一个有限状态集合；Ｉ?Ｓ是初始状态集合；Ｐ是一个原子命题集合；Ｒ?Ｓ×Ｓ表示迁移关系；Ｌ：Ｓ→２Ｐ是一个标记函数；ｆｆｄ是一个故障特征模型；γ：Ｒ→（｛⊥，｝｜Ｎ｜→｛⊥，｝）是一个满函数，将每条迁移标记上一个故障特征表达式。迁移关系Ｒ是满射，即对于每一个状态ｓ，都存在一个后继状态ｓ′，记作Ｒ（ｓ，ｓ′）。标记函数Ｌ在每个状态上标记出所有在该状态上为真的原子命题。ＦＬＴＳ包含着一个故障特征

【参考文献】：
期刊论文
[1]一种结合线性时序逻辑和故障树的软件安全验证方法[J]. 王飞,沈国华,黄志球,马琳,刘畅,李海峰,廖莉莉.  计算机科学. 2015(12)
[2]故障树领域本体及SWRL规则的构建方法研究[J]. 周亮,黄志球,黄传林.  计算机科学. 2015(08)
[3]软件模型检测中的抽象模型研究综述[J]. 魏欧,石玉峰,徐丙凤,黄志球,陈哲.  计算机研究与发展. 2015(07)
[4]软件产品线可变性建模技术系统综述[J]. 聂坤明,张莉,樊志强.  软件学报. 2013(09)



本文编号：3586212