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

范亞瓊，陳海燕

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

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

范亞瓊，陳海燕

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

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

順序邏輯；端口映射表；最小割序集；轉換規則；定性分析

0 引 言

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

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

1 問題描述

對軟件失效行為進行安全性分析的目的是尋找導致軟件系統失效的關鍵事件集合，即最小割序集[7]。作為反映構件失效邏輯層次關系的邏輯門，是定性分析的關鍵所在。

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

對于狀態事件混合邏輯門，其狀態與事件存在順序關系，當衛式條件成立時，失效事件的發生導致邏輯門產生輸出，當衛士條件不成立時，失效事件的發生不會導致邏輯門產生輸出。

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

在狀態事件故障樹中，頂層事件的發生依賴于基本事件的發生順序，而邏輯門中的衛式條件決定了發生的基本事件是否能對全局系統失效產生影響。提出了基于順序邏輯[8]的SEFT定性分析模型，通過記錄構件與邏輯門的交互端口，將邏輯門轉換成布爾邏輯表達式，根據順序邏輯轉換規則，分析引起系統失效的最小關鍵狀態事件序列。

2.1 端口映射表

構件與外界環境的交互分為三種：構件與構件之間的觸發交互、構件與邏輯門的交互、邏輯門與邏輯門的交互。對SEFT進行定性分析，只需關注引起系統失效的關鍵事件或狀態，對于構件內部的行為活動，若不產生外部輸出，則不影響定性分析的結果。構件與外界環境的交互通過輸入輸出端口實現，因此，通過端口映射表建立構件和邏輯門與外界交互的關系。端口映射表的建立分三步完成：

(1)當系統規模較大時，為了方便引用，對構件和邏輯門進行編號。

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

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

2.2 邏輯門轉換規則

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

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

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

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

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

2.3 順序邏輯轉換規則

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

分配規則：

交換規則：

E1∨E2?E2∨E1

最小化規則：

S1∨S2ifS1?S2?S1

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

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

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

(1)當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

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

其余順序邏輯轉換規則，同理可證。

3 實例驗證

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

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

圖1 火災防護系統

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

表1 組件編號表

表2 邏輯門編號表

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

表3 組件端口映射表

表4 邏輯門端口映射表

第三步：將邏輯門轉換成邏輯表達式。

第四步：結合端口映射表，自上到下轉換成系統失效的順序邏輯表達式，并根據順序邏輯轉換規則進行化簡。

G1out1=(G1in2

第五步：導致系統失效的最小割序集為：

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 評價結果及分析

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

(SD1.smokedetect

(SD1.smokedetect

(SD2.smokedetect

(SD2.smokedetect

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

5 結束語

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

實驗結果表明，該方法不僅可以獲得導致系統失效的最小割序集，而且可以反映事件和狀態之間的優先關系，驗證了方法的可行性、可靠性，為SEFT的定性分析方法提供了新思路。

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

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

[3] 郭 勇.基于構件的軟件系統的可靠性評估方法研究[D].哈爾濱:哈爾濱工業大學,2013.

[4] 劉 東.空間信息處理系統可靠性設計與分析關鍵技術研究[D].長沙:國防科學技術大學,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] 徐丙鳳.構件化嵌入式軟件安全性分析方法研究[D].南京:南京航空航天大學,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] 李彥鋒.復雜系統動態故障樹分析的新方法及其應用研究[D].成都:電子科技大學,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] 徐丙鳳,黃志球,胡 軍,等.一種狀態事件故障樹的定量分析方法[J].電子學報,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] 覃慶努.復雜系統可靠性建模、分析和綜合評價方法研究[D].北京:北京交通大學,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 網絡出版時間：2017-07-05

國家“十三五”重點基礎科研項目(JCKY2016206B001)；江蘇省六大人才高峰項目(XXRJ-004)；軟件新技術與產業化協同創新中心資助項目

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

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