分布式離散事件系統的安全可診斷性算法

2018-11-06 03:39:02歐陽丹彤羅知雨耿雪娜張立明

吉林大學學報(理學版) 2018年3期

歐陽丹彤, 羅知雨, 耿雪娜, 張立明

(1. 吉林大學計算機科學與技術學院, 符號計算與知識工程教育部重點實驗室, 長春 130012; 2. 長春理工大學計算機科學與技術學院, 長春 130022)

基于模型診斷(model-based diagnosis, MBD)方法具有設備獨立性、易更新和維護等特點, 因此已逐漸成為故障診斷領域的核心方法, 很多領域都使用該方法進行系統診斷[1], 而且MBD問題可以轉換為可滿足性(SAT)[2-3]問題, 或使用文獻[4]的方法進行求解. 文獻[4]給出了可診斷性的充要條件. 在MBD中, 模型是否正確影響診斷的效果及效率, 不同模型條件下的可診斷性主要針對不同系統下的可診斷性問題. 常見的系統模型有離散事件系統(discrete event systems, DES)[5]、模糊DES[4]及分布式DES[6]等. 由于系統的復雜性逐漸增加, 模型的規模也逐漸增加, 為了降低模型規模及復雜系統的計算量, 人們提出了分布式系統. 在分布式系統中, 為了解決對大規模系統的全局模型進行可診斷性分析的困難, 全局模型被分割成多個有相同通信事件的局部模型或組件, 每個局部模型獨立分析其可診斷性, 由于硬件原因, 局部可診斷性與全局可診斷性不一定相同, 因此分布式系統通過通信事件進行同步, 以獲得全局模型的可診斷性. 一些經典的DES診斷方法同樣在分布式系統診斷中使用, 如診斷器[4]、同步[7]等方法. 同時, 對分布式系統的診斷方法進行了許多改進[8-10], 從而更快速、更準確地判定系統的可診斷性.

盡管在故障發生一段時間后可診斷的系統才能檢測到該故障發生, 但如果沒有及時完成檢測, 則發生的故障可能會危害系統本身及人身財產安全. 為了避免安全事件的發生, 人們希望在系統執行被禁止事件序列前檢測到故障的發生, 基于此, Paoli等[11]提出了判定DES的安全可診斷性. 在文獻[11]的基礎上, 劉富春等[12-14]提出了判定模糊DES、隨機DES的安全可診斷性問題及對DES安全可診斷性的改進算法.

本文提出一種分布式DES的安全可診斷性算法. 對于給定的分布式系統及被禁止事件序列集合, 首先使用同步[4]的方法得到系統的全局模型, 然后判斷系統對給定故障是否可診斷, 確定系統對給定故障可診斷后, 構建系統對給定故障及相應被禁止事件集合的安全診斷器來判斷系統在故障發生后是否發生被禁止事件序列, 假設未發生故障或故障發生后未發生被禁止事件序列, 則系統是可診斷的且是安全可診斷的, 否則系統不是安全可診斷的.

1 預備知識

1.1 分布式離散事件系統及其可診斷性

圖1 由3個局部模型構成的系統S1Fig.1 System S1 composed of three local models

定義1(局部模型)[6]第i個局部模型Γi定義為一個有限狀態自動機Γi=(Qi,Ei,Ti,q0i), 其中:Qi為有限狀態的集合;Ei為事件的集合, 包含3個互不相交的集合, 分別為故障事件集合Fi、可觀測事件集合Oi和通信事件集合Ci;Ei,Oi,Fi只發生在Γi中;Ti為轉移函數集合,Ti?Qi×Ei×Qi;q0i為系統的初始狀態.

其中:ψ表示同步事件集合且ε?ψ;ev(ti)表示ti的事件標簽.

圖2 局部模型Γ2自同步得到的系統GFig.2 System G obtained by self-synchronizing local model Γ2

圖2為圖1中Γ2的診斷器以可觀測事件為同步事件, 自同步得到系統G. 系統內不同的局部模型間通過兩個局部模型間相同的通信事件進行同步轉換, 可得到系統的全局模型. 假設系統由n(n≥1)個局部模型組成, 則系統{Γ1,Γ2,…,Γn}的全局模型定義如下.

Cj為通信事件.

定義3(局部可診斷性)[6]若局部模型Γ中發生故障fi后又發生了有限個可觀測事件, 則fi在該局部模型中是可診斷的, 即fi是局部可診斷的, 即

其中:pf表示以初始狀態p0為起點, 以fi發生后的狀態為終點的路徑;sf表示pf的后續路徑; Obs表示可觀測投影的映射函數; Obs-1表示可觀測投影的逆映射函數[2].

由文獻[6]知, 如果fi是局部可診斷的, 則fi是全局可診斷的.

1.2 離散事件系統的安全可診斷性

系統中可以發生多類故障事件, 每類故障事件包含多個故障事件, 假設對于第i類型故障fi的被禁止事件序列集合為Φi,Φi∈E*, 其中E*為E的閉包[2]. 為了滿足安全性, 在某類故障fi發生后, 避免系統執行Φi.

其中[s∈Ψ(Efi)](i=1,2,…,m)}([v∈Φi,v為u的子序列]),

其中:Ψ(Efi)表示以第i類故障事件結尾的路徑;L/s表示語言L中發生在事件s的后續路徑.

如果一個系統是安全可診斷的, 則該系統首先是可診斷的.

定義5(可診斷性)[4]語言L可診斷的條件如下:

(?i∈Πf)(?ni∈)(?s∈Ψ(Efi))(?t∈L/s)(‖t‖≥ni?D),

其中D為ω∈Obs-1[Obs(st)]?Efi∈ω.

定義6(Fi確定與不確定性)[4]若診斷器中存在狀態q, ?(x,l)∈q滿足Fi∈l, 則稱q是Fi確定的. 反之, 若診斷器中存在狀態q,?(x,l),(y,l′)∈q且Fi∈l,Fi?l′, 則稱q是Fi不確定的.

定義7(安全可診斷)[11]語言L安全可診斷的條件如下:

1) 可診斷性條件同定義5;

2 安全診斷器的構造

定義8(非法語言標簽)[11]非法語言的標簽函數為

其中：Bi表示故障發生后又執行了相應的被禁止事件串;S表示無故障事件發生或故障事件發生后未執行相應的被禁止事件.

通過非法語言的標簽函數能構造系統的非法語言識別器.

定義9(非法語言識別器) 對系統Γi中發生的故障fi及對應的被禁止事件集合Φi構造的非法語言識別器Gr為有限狀態自動機Gr={Qr,E,Tr,q0r}, 其中：Qr為狀態空間,

Qr∈Q×πl(s),πl(s)=π(s)×l(s),

l(s)為故障標簽,

q0r=(ε,N-S);Tr：Qr×E×Qr為狀態轉換函數,

Tr((s,πl(s)),σ)=(t,πl(t)),s,t∈Qr,σ∈E,

轉換規則為

通過非法語言識別器可獲得添加安全標簽的自動機：

Γm=Γi×G1×…×Gm=(Qm,E,Tm,q0m),

其中Γm中的一個狀態

z=[q,(s1,π(s1)),…,(sm,π(sm))].

圖3為G對f2,{o3}構造的非法語言識別器Gr.

定義10(安全診斷器) 若存在自動機γ=(Q,E,T,q0), 則該自動機對fi和Φi的安全診斷器為

圖3 非法語言識別器GrFig.3 Illegal language recognizer Gr

圖4 安全診斷器

1)q為Fi不確定狀態;

2)q,q′狀態如下:

①q為Fi確定狀態;

②q′為Fi不確定狀態.

因圖4中存在F2不確定狀態[(y3,F2-B2),(y3,N-S)], 因此由定理1知該系統不是安全可診斷的.

3 分布式離散事件系統判定安全可診斷算法

3.1 分布式離散事件系統的安全可診斷性

判斷系統是否安全可診斷前, 首先需將局部模型通過同步操作構成系統的全局模型, 根據定義2, 可由下列算法構建系統的全局模型.

算法1構建全局模型算法.

Function: GS( );

Input: 局部模型{Γ1,Γ2,…,Γn};

Output:Γ;

if 系統安全可診斷, return系統可診斷;

if系統不可診斷, return 系統不可診斷;

Begin

1) Initialization:A←{Γ1,Γ2,…,Γn}{Γi};

2) whileA≠? do

3) 從A取出與Γ1有相同通信事件Ci的Γi;

4)Γi←Synch(Γi,Γj,Sync(ti,tj),Ci);

5) end while

6) AbstractKeyPath(Γi);

7)Γ←Γi;

8) DR(Γ);

9) Check1(Γ);

End.

算法1中步驟4)使用函數Synch(Γi,Γj,Sync(ti,tj))先將兩個局部模型同步獲得一個新的模型, 再將結果保存在Γi中；步驟6)中AbstractKeyPath(Γi)為對系統剪枝保留關鍵路徑, 即只保留包含故障的語言及可診斷性與其相同的語言; 步驟8)中DR(Γ)為構建診斷器；步驟9)中Check1(Γ)為檢查系統是否安全可診斷, Check1( )可能有兩種結果：

1) 若系統包含Fi不確定狀態環, 則返回系統不可診斷;

2) 若系統不包含Fi不確定狀態環, 則返回系統可診斷.

若系統可診斷, 則根據定義8和定理1構建系統的安全診斷器, 用以判斷系統是否安全可診斷.

算法2安全可診斷性判斷算法.

Function: SDR( );

Inputs:Γ;

故障事件fi;

被禁止事件集合Φi;

Outputs: if 系統安全可診斷, return系統安全可診斷;

if 系統不可安全診斷, return系統不可安全診斷;

Begin

1) Lable(Γ);