范亞瓊，陳海燕

(南京航空航天大學(xué) 計算機科學(xué)與技術(shù)學(xué)院,江蘇 南京 210016)

基于順序邏輯的狀態(tài)事件故障樹定性分析模型

范亞瓊，陳海燕

(南京航空航天大學(xué) 計算機科學(xué)與技術(shù)學(xué)院,江蘇 南京 210016)

針對現(xiàn)有的狀態(tài)事件故障樹(SEFT)定性分析方法在反映失效系統(tǒng)中構(gòu)件狀態(tài)與事件邏輯順序關(guān)系方面的不足，提出了基于順序邏輯的狀態(tài)事件故障樹定性分析模型。該模型通過建立構(gòu)件與邏輯門的端口映射表，定義邏輯門到布爾邏輯的轉(zhuǎn)換規(guī)則限定狀態(tài)和事件的次序關(guān)系，根據(jù)順序邏輯轉(zhuǎn)換規(guī)則獲得導(dǎo)致系統(tǒng)失效的狀態(tài)事件序列(最小割序集)，以解決系統(tǒng)失效應(yīng)滿足的狀態(tài)與事件的邏輯順序關(guān)系問題。為驗證所提出模型的有效性和可行性，以火災(zāi)防護系統(tǒng)為研究對象進行了實例驗證實驗。實驗結(jié)果表明，所提出的模型有效可行，所獲得的最小割序集能夠反映各失效事件和狀態(tài)間的順序邏輯關(guān)系，分析結(jié)果符合客觀實際，為SEFT的定性分析提供了一種新的技術(shù)途徑和方法借鑒。

順序邏輯；端口映射表；最小割序集；轉(zhuǎn)換規(guī)則；定性分析

0 引 言

狀態(tài)事件故障樹[1](State/Event Fault Tree，SEFT)是基于軟件的構(gòu)件設(shè)計模型建立的一種表達系統(tǒng)失效行為的安全性分析模型。與傳統(tǒng)的故障樹[2-4]不同的是，狀態(tài)事件故障樹具有構(gòu)件化和基于狀態(tài)的特性，且嚴(yán)格區(qū)分了狀態(tài)、事件語義，增加了狀態(tài)依賴的表達。因此，對狀態(tài)事件故障樹進行最小割序集分析不僅要關(guān)注構(gòu)件失效的集合，也要關(guān)注構(gòu)件失效事件和狀態(tài)間的順序關(guān)系，即分析出最小割序集。目前國內(nèi)外安全分析領(lǐng)域的研究人員對SEFT的定性分析進行了相關(guān)研究。Michael Roth[5-6]提出將SEFT轉(zhuǎn)換到確定隨機Petri網(wǎng)(Deterministic and Stochastic Petri Nets，DSPN)，在DSPN的基礎(chǔ)上計算其順序邏輯并分析導(dǎo)致系統(tǒng)失效的最小割序集，但是該最小割序集只關(guān)注失效事件，未涉及失效事件發(fā)生時相關(guān)構(gòu)件應(yīng)滿足的狀態(tài)；徐博士[7]提出基于接口自動機的軟件失效行為安全性分析模型。該模型考慮構(gòu)件狀態(tài)作為衛(wèi)式條件對邏輯門輸出產(chǎn)生的影響，計算過程繁瑣，且最小割序集中未能反映狀態(tài)和事件間的次序關(guān)系。

為此，提出了基于順序邏輯的狀態(tài)事件故障樹定性分析模型。該模型通過分析構(gòu)件與外界環(huán)境交互的狀態(tài)或事件，建立邏輯門與構(gòu)件端口相關(guān)聯(lián)的端口映射表，定義邏輯門的轉(zhuǎn)換規(guī)則，通過擴展布爾邏輯提出順序邏輯轉(zhuǎn)換規(guī)則，自頂向下計算分析整體系統(tǒng)的失效序列，通過化簡操作獲得系統(tǒng)的最小割序集。

1 問題描述

對軟件失效行為進行安全性分析的目的是尋找導(dǎo)致軟件系統(tǒng)失效的關(guān)鍵事件集合，即最小割序集[7]。作為反映構(gòu)件失效邏輯層次關(guān)系的邏輯門，是定性分析的關(guān)鍵所在。

在SEFT中，構(gòu)件的狀態(tài)雖不能和事件一樣觸發(fā)邏輯門輸出的發(fā)生，但是它可以允許或禁止邏輯門輸出的發(fā)生。在進行SEFT定性分析的過程中，需要同時考慮構(gòu)件的基本事件以及部分可作為衛(wèi)式的構(gòu)件狀態(tài)。

對于狀態(tài)事件混合邏輯門，其狀態(tài)與事件存在順序關(guān)系，當(dāng)衛(wèi)式條件成立時，失效事件的發(fā)生導(dǎo)致邏輯門產(chǎn)生輸出，當(dāng)衛(wèi)士條件不成立時，失效事件的發(fā)生不會導(dǎo)致邏輯門產(chǎn)生輸出。

2 基于順序邏輯的SEFT定性分析模型

在狀態(tài)事件故障樹中，頂層事件的發(fā)生依賴于基本事件的發(fā)生順序，而邏輯門中的衛(wèi)式條件決定了發(fā)生的基本事件是否能對全局系統(tǒng)失效產(chǎn)生影響。提出了基于順序邏輯[8]的SEFT定性分析模型，通過記錄構(gòu)件與邏輯門的交互端口，將邏輯門轉(zhuǎn)換成布爾邏輯表達式，根據(jù)順序邏輯轉(zhuǎn)換規(guī)則，分析引起系統(tǒng)失效的最小關(guān)鍵狀態(tài)事件序列。

2.1 端口映射表

構(gòu)件與外界環(huán)境的交互分為三種：構(gòu)件與構(gòu)件之間的觸發(fā)交互、構(gòu)件與邏輯門的交互、邏輯門與邏輯門的交互。對SEFT進行定性分析，只需關(guān)注引起系統(tǒng)失效的關(guān)鍵事件或狀態(tài)，對于構(gòu)件內(nèi)部的行為活動，若不產(chǎn)生外部輸出，則不影響定性分析的結(jié)果。構(gòu)件與外界環(huán)境的交互通過輸入輸出端口實現(xiàn)，因此，通過端口映射表建立構(gòu)件和邏輯門與外界交互的關(guān)系。端口映射表的建立分三步完成：

(1)當(dāng)系統(tǒng)規(guī)模較大時，為了方便引用，對構(gòu)件和邏輯門進行編號。

(2)對于每個構(gòu)件，記錄與外界環(huán)境交互的關(guān)鍵事件或狀態(tài)，若每個構(gòu)件的交互端口較少，只需建立一個表存放所有的構(gòu)件交互行為，若構(gòu)件的交互端口較多，可為每一個構(gòu)件建立一個組件端口映射表，表中說明構(gòu)件編號、源端口、目的端口、狀態(tài)事件類型、輸入輸出方向、具體行為。

(3)對每個邏輯門，記錄與外界交互的端口，若每個邏輯門的交互端口較少，只需建立一張表存放所有的邏輯門交互行為，若邏輯門的交互端口較多，可為每一個邏輯門建立一張邏輯門端口映射表，表中說明邏輯門編號、源端口、目的端口、狀態(tài)事件類型、數(shù)據(jù)流向。

2.2 邏輯門轉(zhuǎn)換規(guī)則

在SEFT的邏輯門[9]中，狀態(tài)不能和事件一樣觸發(fā)邏輯門輸出的發(fā)生，但是狀態(tài)可以允許或者禁止邏輯門輸出的發(fā)生。當(dāng)所有的衛(wèi)式條件都為真時，邏輯門才能觸發(fā)。為了反映狀態(tài)和事件之間的區(qū)別，所有邏輯門的輸入和輸出都標(biāo)識了狀態(tài)和事件端口類型。引入符號<表示先后次序關(guān)系，事件類型用E表示，狀態(tài)類型用S表示。對SEFT的邏輯門類型及其轉(zhuǎn)換規(guī)則描述如下：

(1)狀態(tài)與門(State-AND Gate)：具有一個狀態(tài)類型的輸出和一個或者多個狀態(tài)類型的輸入。它所表示的語義是當(dāng)所有的輸入表達式都滿足時，輸出狀態(tài)才會為真。其中輸出狀態(tài)S唯一，輸入狀態(tài)的個數(shù)n是任意的，且所有輸入的順序是可交互換的，其轉(zhuǎn)換規(guī)則為S=[S1∧S2∧…∧Sn]。

(2)事件狀態(tài)混合與門(Event/state-AND Gate)：具有一個事件E1輸入和n個狀態(tài)(S1…Sn)輸入，輸出為事件類型，通常第一個輸入是事件類型。該邏輯門的語義為當(dāng)輸入事件觸發(fā)，并且輸入的狀態(tài)表達式都滿足時，輸出事件被觸發(fā)。其轉(zhuǎn)換規(guī)則為E=[S1∧S2∧…∧Sn]

(3)狀態(tài)或門(State-OR Gate)：具有一個狀態(tài)類型的輸出和一個或者多個狀態(tài)類型的輸入。它的語義為當(dāng)一個或者多個輸入表達式得到滿足時，輸出狀態(tài)為真。其中輸入的狀態(tài)個數(shù)n是任意的，且所有輸入狀態(tài)的順序是可交換的。其轉(zhuǎn)換規(guī)則為S=[S1∨S2∨…∨Sn]。

(4)優(yōu)先與門(Priority-AND Gate)：具有事件類型的輸出和一個或者多個事件類型的輸入。它的語義為當(dāng)輸入事件以從左到右的順序依次發(fā)生時，輸出事件被觸發(fā)。其轉(zhuǎn)換規(guī)則為E=E1

2.3 順序邏輯轉(zhuǎn)換規(guī)則

通過端口映射表和邏輯門轉(zhuǎn)換規(guī)則可以獲得由構(gòu)件狀態(tài)和事件組成的全局邏輯表達式。對布爾邏輯規(guī)則進行擴展，提出順序邏輯轉(zhuǎn)換規(guī)則[10-13]，對全局邏輯表達式進行化簡，獲得引起系統(tǒng)失效的最小割序集。

分配規(guī)則：

交換規(guī)則：

E1∨E2?E2∨E1

最小化規(guī)則：

S1∨S2ifS1?S2?S1

接下來對分配規(guī)則(S1∨S2)

用α,β,γ表示失效狀態(tài)或事件，所有事件和狀態(tài)構(gòu)成的非空集合為Ω，α,β,γ∈Ω，t(α)表示事件或狀態(tài)的發(fā)生時間，若t(α)

σ定義了一個從Ω到{0,1}的映射，其含義是：如果事件A未在規(guī)定的時間區(qū)間[0,T]內(nèi)失效，不管以后其失效與否，都認(rèn)為其真值為0；反之為1。

(1)當(dāng)t(α)

(2)任取2個大于T，也容易得到等號兩邊賦值均為0；

(3)任取一個大于T，考慮6種情形：

①0≤t(γ)≤t(β)≤T

②0≤t(β)≤t(γ)≤T

③0≤t(α)≤t(γ)≤T

④0≤t(γ)≤t(α)≤T

⑤0≤t(α)≤t(β)≤T

⑥0≤t(β)≤t(α)≤T

通過證明可得，左右兩邊賦值均相同，且無永真式或永假式。滿足等價性定理。

其余順序邏輯轉(zhuǎn)換規(guī)則，同理可證。

3 實例驗證

圖1給出一個火災(zāi)防護系統(tǒng)的SEFT定性分析實例。頂層事件表示火災(zāi)防護系統(tǒng)的失效，PAND門的輸出表示檢測到火災(zāi)，OR2的輸出表示噴淋系統(tǒng)失效。該SEFT所描述的危害為：當(dāng)感煙傳感器和感溫傳感器都相繼檢測到火災(zāi)，但是噴淋系統(tǒng)失效，最終導(dǎo)致火災(zāi)發(fā)生。

該系統(tǒng)含有7個構(gòu)件，分別是感煙傳感器SD1和SD2，感溫傳感器HD，溫度傳感器TS，噴嘴N1和N2，水泵P。另外，含有6個邏輯門，分別為AND3，PAND，OR2，OR1，AND1，AND2。下面將逐步介紹最小割序集的生成過程。

圖1 火災(zāi)防護系統(tǒng)

第一步：對SEFT的所有邏輯門和組件進行編號，見表1和表2。

表1 組件編號表

表2 邏輯門編號表

第二步：為每個邏輯門和組件建立端口映射表，見表3和表4。

表3 組件端口映射表

表4 邏輯門端口映射表

第三步：將邏輯門轉(zhuǎn)換成邏輯表達式。

第四步：結(jié)合端口映射表，自上到下轉(zhuǎn)換成系統(tǒng)失效的順序邏輯表達式，并根據(jù)順序邏輯轉(zhuǎn)換規(guī)則進行化簡。

G1out1=(G1in2

第五步：導(dǎo)致系統(tǒng)失效的最小割序集為：

P.S<(SD1.smokedetect<(TS.S

P.S<(SD2.smokedetect<(TS.S

(N1.S∧N2.S)<(SD1.smokedetect<(TS.S

(N1.S∧N2.S)<(SD2.smokedetect<(TS.S

4 評價結(jié)果及分析

為了分析基于順序邏輯SEFT定性分析方法的可行性、可靠性及優(yōu)缺點，采用基于接口自動機的軟件失效行為安全性分析方法[13-14]對該火災(zāi)防護系統(tǒng)進行定性分析，評價結(jié)果如下所示：

(SD1.smokedetect

(SD1.smokedetect

(SD2.smokedetect

(SD2.smokedetect

基于接口自動機的定性分析方法僅能獲得基本事件的失效序列，如上述割序集(SD.smokedetect

5 結(jié)束語

針對現(xiàn)有的SEFT定性分析方法中未能體現(xiàn)狀態(tài)與事件的順序邏輯關(guān)系問題，提出了基于順序邏輯的狀態(tài)事件故障樹定性分析模型。通過分析構(gòu)件內(nèi)部時序活動對系統(tǒng)失效的影響，將構(gòu)件與外界交互的狀態(tài)或事件記為可能對系統(tǒng)失效產(chǎn)生影響的候選事件或狀態(tài)，符合客觀實際。同時，定義邏輯門的轉(zhuǎn)換規(guī)則，獲得由構(gòu)件狀態(tài)和事件組成的全局邏輯表達式，根據(jù)順序邏輯規(guī)則化簡得到最小割序集。

實驗結(jié)果表明，該方法不僅可以獲得導(dǎo)致系統(tǒng)失效的最小割序集，而且可以反映事件和狀態(tài)之間的優(yōu)先關(guān)系，驗證了方法的可行性、可靠性，為SEFT的定性分析方法提供了新思路。

[1] Kaiser B. State event trees: a safety and reliability analysis techniqure for software controlled systems[D].Kaiserslautern:University of Kaiserslautern,2007.

[2] 劉文彬.基于模塊化思想的動態(tài)故障樹分析方法研究[D].南京:南京理工大學(xué),2009.

[3] 郭 勇.基于構(gòu)件的軟件系統(tǒng)的可靠性評估方法研究[D].哈爾濱:哈爾濱工業(yè)大學(xué),2013.

[4] 劉 東.空間信息處理系統(tǒng)可靠性設(shè)計與分析關(guān)鍵技術(shù)研究[D].長沙:國防科學(xué)技術(shù)大學(xué),2008.

[5] Roth M R,Liggesmeyer P.Qualitative analysis of state/event fault trees for supporting the certification process of software-intensive systems[C]//IEEE international symposium on software reliability engineering workshops.[s.l.]:IEEE,2013:353-358.

[6] Roth M,Hartoyo A,Liggesmeyer P.Efficient reachability gr-aph development for qualitive analysis of state/event fault trees[C]//IEEE international symposium on software reliability engineering workshops.[s.l.]:IEEE,2015:144-151.

[7] 徐丙鳳.構(gòu)件化嵌入式軟件安全性分析方法研究[D].南京:南京航空航天大學(xué),2014.

[8] Roth M,Liggesmeyer P.Sequential logic for state/event fault trees:a methodology to support the failure modeling of cyber physical systems[C]//International conference on computer safety,reliability,and security.[s.l.]:Springer International Publishing,2015:121-132.

[9] 李彥鋒.復(fù)雜系統(tǒng)動態(tài)故障樹分析的新方法及其應(yīng)用研究[D].成都:電子科技大學(xué),2013.

[10] Guck D,Han T,Katoen J P,et al.Quantitative timed analysis of interactive Markov chains[C]//NASA formal methods symposium.[s.l.]:[s.n.],2012:8-23.

[11] 徐丙鳳,黃志球,胡 軍,等.一種狀態(tài)事件故障樹的定量分析方法[J].電子學(xué)報,2013,41(8):1480-1486.

[12] Tang Z,Dugan J B.Minimal cut set/sequence generation for dynamic fault trees[C]//Annual symposium on reliability and maintainability.Charlottesville,USA:IEEE,2004:207-213.

[13] 覃慶努.復(fù)雜系統(tǒng)可靠性建模、分析和綜合評價方法研究[D].北京:北京交通大學(xué),2012.

[14] Boudali H,Crouzen P M.A rigorous,compositional,and extensible framework for dynamic fault tree analysis[J].IEEE Transactions on Dependable and Secure Computing,2010,7(2):128-143.

Qualitative Analysis Model of State/Event Fault Tree with Sequential Logic

FAN Ya-qiong，CHEN Hai-yan

(Department of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

In order to overcome the shortcomings of reflecting the relationship between component state and sequential logic in failure system for State/Event Fault Tree (SEFT) qualitative analysis method,a qualitative analysis model of state event fault tree based on sequential logic is proposed.It defines transition rule of logic gate to Boolean logic to define the order of state and event by establishment of the port mapping table of components and logic gates,and gets the sequence of state events (minimum cut sequence set) that leads to system failure according to sequential logic transformation rules to solve the problem of logic order of state and event for system failure.In order to verify the validity and feasibility of the proposed model,a fire protection system has been established as an example of object for verification experiment.It is indicated that the cut order set can reflect the sequential logic relation between the failure event and the state.The feasibility of this model has been verified,which is consistent with the objective reality.Therefore,a new effective approach is provided for the qualitative analysis of SEFT.

sequential logic;port mapping table;minimum cut sequence set;conversion rules;qualitative analysis

2016-08-13

2016-11-23 網(wǎng)絡(luò)出版時間：2017-07-05

國家“十三五”重點基礎(chǔ)科研項目(JCKY2016206B001)；江蘇省六大人才高峰項目(XXRJ-004)；軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心資助項目

范亞瓊(1990-)，女，碩士研究生，研究方向為軟件工程、系統(tǒng)建模與仿真;陳海燕，講師，研究方向為數(shù)據(jù)挖掘、民航信息化等。

http://kns.cnki.net/kcms/detail/61.1450.TP.20170705.1650.032.html

TP311

A

1673-629X(2017)08-0012-04

10.3969/j.issn.1673-629X.2017.08.003