故障樹分析是提高系統(tǒng)安全性和可靠性的有效方法。傳統(tǒng)的人工故障樹生成方式難以解決當(dāng)前系統(tǒng)的龐大規(guī)模與復(fù)雜性的問題,且容易出錯(cuò)。為此,提出基于故障配置的故障樹生成方法,引入軟件產(chǎn)品線的可變性管理,用于系統(tǒng)故障建模與形式化分析。首先,定義故障特征圖模型用于刻畫系統(tǒng)故障間的約束關(guān)系,基于Kripke結(jié)構(gòu)定義故障標(biāo)記遷移系統(tǒng)來描述系統(tǒng)的行為;然后,基于模型的語義建立通過模型檢測(cè)生成故障樹的過程;最后,通過時(shí)序邏輯描述系統(tǒng)安全屬性,利用模型檢測(cè)工具SNIP驗(yàn)證安全屬性進(jìn)而生成故障樹。案例研究驗(yàn)證了該方法的有效性。 

【文章來源】：計(jì)算機(jī)科學(xué). 2017,44(02)北大核心CSCD

【文章頁數(shù)】：10 頁

【部分圖文】：

圖１數(shù)據(jù)采集器系統(tǒng)

偏離故障，則數(shù)據(jù)值每次增加２，且不再進(jìn)行重置。該故障為瞬時(shí)性故障（ＴｒａｎｓｉｅｎｔＦａｕｌｔ），即組件發(fā)生故障后可能會(huì)恢復(fù)正常。２）傳感器單元也可能發(fā)生固定型故障。當(dāng)傳感器發(fā)生癱瘓后，采集到的數(shù)據(jù)值會(huì)保持為一個(gè)固定的值不再發(fā)生變化。該故障一旦發(fā)生，其影響是永久性的（ＰｅｒｍａｎｅｎｔＦａｕｌｔ），組件無法再恢復(fù)正常。３）過濾器單元可能發(fā)生與傳感器單元類似的固定型故障，過濾器單元的數(shù)據(jù)保持為固定數(shù)值而不再變化，該故障屬于永久性故障。數(shù)據(jù)采集器系統(tǒng)的故障特征圖如圖３所示。故障特征圖是一種樹狀圖，圖中的每一個(gè)節(jié)點(diǎn)表示一個(gè)故障特征，其中根節(jié)點(diǎn)表示數(shù)據(jù)采集器系統(tǒng)的故障；葉節(jié)點(diǎn)表示系統(tǒng)元件的基本故障；中間節(jié)點(diǎn)表示系統(tǒng)模塊的故障。故障特征圖中的邊刻畫了故障特征間的約束關(guān)系，圖３示例表示的是與關(guān)系、或關(guān)系等。圖３中，特征Ｓ１和Ｓ２以與關(guān)系連接到特征ＳＳ，表示傳感器模塊的故障包括優(yōu)先和備份傳感器單元的故障；特征Ｓ１ＤＴ和Ｓ１ＳＰ表示優(yōu)先傳感器可能發(fā)生的故障，二者均標(biāo)記為可選且以與關(guān)系連接，表示在系統(tǒng)運(yùn)行過程中二者互不影響，從而可能出現(xiàn)３種情況，即二者都發(fā)生、其中之一發(fā)生或都不發(fā)生；特征Ｓ２ＤＴ和Ｓ２ＳＰ也為可選故障，但與前面不同的是二者以異或關(guān)系連接到特征Ｓ２，表示在系統(tǒng)的一次運(yùn)行過程中，備份傳感器單元的這兩種故障不會(huì)同時(shí)出現(xiàn)。圖３數(shù)據(jù)采集器系統(tǒng)故障特征圖現(xiàn)有的安全性分析技術(shù)在對(duì)故障建模時(shí)通常只是描述其起源、傳播或具體行為，而沒有對(duì)故障間的約束關(guān)系進(jìn)行刻１８４計(jì)算機(jī)科學(xué)２０１７年

配置（ＦａｕｌｔＣｏｎｆｉｇｕｒａｔｉｏｎ）。故障特征圖的語義即所有合法的系統(tǒng)故障配置的集合記作［［ｆｆｄ］］ＦＦＤ，且［［ｆｆｄ］］ＦＦＤ?｛２Ｆ｝。以數(shù)據(jù)采集器系統(tǒng)為例，如圖３所示，根據(jù)故障特征圖的語法，數(shù)據(jù)采集器系統(tǒng)的故障特征集合為Ｆａｕｌｔ＝｛Ｓ１ＳＰ，Ｓ１ＤＴ，Ｓ２ＳＰ，Ｓ２ＤＴ，Ｆ１ＳＰ，Ｆ２ＳＰ｝，而系統(tǒng)所有的故障配置集合為｛２Ｆａｕｌｔ｝。３．２故障標(biāo)記遷移系統(tǒng)傳統(tǒng)的模型檢測(cè)過程通常采用狀態(tài)遷移系統(tǒng)對(duì)系統(tǒng)行為進(jìn)行建模。Ｋｒｉｐｋｅ結(jié)構(gòu)［２１］是一種常用的系統(tǒng)模型，包含系統(tǒng)狀態(tài)和系統(tǒng)狀態(tài)遷移關(guān)系。為了對(duì)包含故障特征的系統(tǒng)行為進(jìn)行分析，本文對(duì)Ｋｒｉｐｋｅ結(jié)構(gòu)進(jìn)行拓展并提出故障標(biāo)記遷移系統(tǒng)（ＦａｕｌｔＬａｂｅｌｅｄＴｒａｎｓｉｔｉｏｎＳｙｓｔｅｍ，ＦＬＴＳ），通過在遷移關(guān)系上添加特征標(biāo)記來區(qū)分遷移關(guān)系描述的行為。故障標(biāo)記遷移系統(tǒng)的形式化定義如下。定義５一個(gè)ＦＬＴＳ是一個(gè)元組ｆｌｔｓ＝（Ｓ，Ｉ，Ｐ，Ｒ，Ｌ，ｆｆｄ，γ），其中：Ｓ是一個(gè)有限狀態(tài)集合；Ｉ?Ｓ是初始狀態(tài)集合；Ｐ是一個(gè)原子命題集合；Ｒ?Ｓ×Ｓ表示遷移關(guān)系；Ｌ：Ｓ→２Ｐ是一個(gè)標(biāo)記函數(shù)；ｆｆｄ是一個(gè)故障特征模型；γ：Ｒ→（｛⊥，｝｜Ｎ｜→｛⊥，｝）是一個(gè)滿函數(shù)，將每條遷移標(biāo)記上一個(gè)故障特征表達(dá)式。遷移關(guān)系Ｒ是滿射，即對(duì)于每一個(gè)狀態(tài)ｓ，都存在一個(gè)后繼狀態(tài)ｓ′，記作Ｒ（ｓ，ｓ′）。標(biāo)記函數(shù)Ｌ在每個(gè)狀態(tài)上標(biāo)記出所有在該狀態(tài)上為真的原子命題。ＦＬＴＳ包含著一個(gè)故障特征

【參考文獻(xiàn)】：
期刊論文
[1]一種結(jié)合線性時(shí)序邏輯和故障樹的軟件安全驗(yàn)證方法[J]. 王飛,沈國華,黃志球,馬琳,劉暢,李海峰,廖莉莉.  計(jì)算機(jī)科學(xué). 2015(12)
[2]故障樹領(lǐng)域本體及SWRL規(guī)則的構(gòu)建方法研究[J]. 周亮,黃志球,黃傳林.  計(jì)算機(jī)科學(xué). 2015(08)
[3]軟件模型檢測(cè)中的抽象模型研究綜述[J]. 魏歐,石玉峰,徐丙鳳,黃志球,陳哲.  計(jì)算機(jī)研究與發(fā)展. 2015(07)
[4]軟件產(chǎn)品線可變性建模技術(shù)系統(tǒng)綜述[J]. 聶坤明,張莉,樊志強(qiáng).  軟件學(xué)報(bào). 2013(09)



本文編號(hào)：3586212