基于事件集的反應系統(tǒng)模型的驗證

張 磊，馬光勝

(1.黑龍江東方學院 計算機科學與電氣工程學部,黑龍江 哈爾濱150008;2.哈爾濱工程大學 計算機科學與技術學院,黑龍江 哈爾濱150003)

本文在沒有其他模型檢測工具的情況下使用UML狀態(tài)圖驗證已建模的反應系統(tǒng)。反應系統(tǒng)在這里認為是面向狀態(tài)并對外部或內部行動做出反應，反應有可能產生狀態(tài)或行為的變化，一個反應系統(tǒng)（事件驅動）的行為由一系列的狀態(tài)、事件和行為集所規(guī)范。

1 提出的驗證技術

1.1 假設

假定正在考慮中的系統(tǒng)有多個合作的對象，這些對象通過事件相互聯(lián)系。每個對象的動態(tài)行為都用UML狀態(tài)圖建模。這些對象在接收一個正確的外部或內部產生事件及相應的保護條件變?yōu)檎鎸崰顟B(tài)發(fā)生改變。要驗證的屬性用時態(tài)邏輯表示并由符號φ代表。驗證過程包括每個UML狀態(tài)圖到一個元組{Si,Ei,Ti,Ii}形式的轉換。其中i代表對象，Si代表非空有限的狀態(tài)集，Ei代表事件集，Ti?Si×Si是一套轉換集。Ii?Si是一套初始狀態(tài)集。讓 Et為總的事件集即 Et={E1∪E2…En},其中 n是系統(tǒng)對象的數量[1]。

1.2 基于事件的驗證方法

一旦在Et中所有事件都發(fā)生時就合并所有對象的狀態(tài)轉換來建造系統(tǒng)的狀態(tài)空間,在狀態(tài)空間 (on the fly)的狀態(tài)圖中找到表示為┐φ的錯誤狀態(tài)(否定行為),如果終止了更深層的狀態(tài)空間的搜索，就會演示出錯誤軌跡（反例）。

本節(jié)中描述的算法[2]如下：

(1)一個事件是相關的如果：

①存在著一個與這個事件相關的轉換并且當前狀態(tài)是一個錯誤狀態(tài)（┐φ）

②存在于一個與這個事件相關的轉換并且下一個狀態(tài)為一個錯誤狀態(tài)（┐φ）

(2)一套事件是相關的如果：

存在著一套與這些事件相關的轉換，并且能將對象從最初狀態(tài)轉到錯誤狀態(tài)（┐φ）。即將對象從一個對象的最初狀態(tài)轉到錯誤狀態(tài)的事件集合叫做相關的事件集。

相關事件集計算完，每個對象的UML狀態(tài)圖都轉換成這種元組{Si,Eri,Ti,Ii}，其中Eri代表聯(lián)系對象 Oi的相關事件集，Ert代表總的相關事件集,即 Ert={Er1∪Er2∪…Ern}。搜索狀態(tài)空間只考慮在總的相關事件集Ert中的事件。一旦到達了錯誤狀態(tài)或訪問了所有的狀態(tài)，就終止搜索狀態(tài)圖。

2 實例研究

(1)火車道口問題是實時系統(tǒng)中的一個典型問題?；疖嚨揽谙到y(tǒng)用來操縱道口的欄桿。對于兩個鐵軌上的門位于區(qū)域 A上，火車在兩個鐵軌（T1,T2）上任意方向運行[3]。圖 1中顯示了已經定位的傳感器(S1,S2,S3,S4和 S5)。傳感器表明當火車行駛到區(qū)域A、進入RC、離開區(qū)域A或退出RC。傳感器S5表明門是關著的還是開著的。“占用期間”指RC上有一個或更多火車的時期。系統(tǒng)被期望滿足如下的屬性：

①道口在所有占用期間是關閉的(安全)；

②如果占用期間沒有火車,道口是開放的(實用性)；

③道口在盡可能的時間里是開放的(活性)。

(2)GRC的UML狀態(tài)圖模型

對象道口欄桿和鐵軌的動態(tài)行為用UML狀態(tài)圖規(guī)范化了，如圖2所示，欄桿的UML狀態(tài)圖顯示了一個最初狀態(tài)和4個簡單狀態(tài)，即開著、正關閉、關閉和正打開。欄桿通過正打開和正關閉對外界信號做出反應[4]。每個正交區(qū)域都有一個最初狀態(tài)和5個簡單狀態(tài)。

2.1 狀態(tài)空間的構建

對象鐵軌有兩個正交狀態(tài)Track1和Track2。對象欄桿有4個局部狀態(tài)，Track1有5個局部狀態(tài)，Track2有5個局部狀態(tài)。GRC系統(tǒng)的 U包括（4×5×5）100個狀態(tài)。通常模型限定可到達狀態(tài)的數量。表1顯示了所有可能的狀態(tài)。

表1 所有可能的狀態(tài)

2.2 基于事件的算法應用到火車道口系統(tǒng)

在GRC模型中要檢測的安全屬性“當火車在Track1或 Track2上的 RC時，道口始終關閉”[5]，時態(tài)邏輯表示為：(T1.Crossing∨T2.Crossing)?G.Closed，如果成立則此模型有漏洞，產生一個反例/錯誤軌跡[3]，否定形式表示為 ：(T1.Crossing∨T2.Crossing)? ┐(G.Closed)，這 就 意 味著火車通過時大門開著或正開著或正關閉的狀態(tài)中。

圖3中，狀態(tài)搜索從最初狀態(tài) S1開始，由事件“tkevarrive”引發(fā)的后續(xù)狀態(tài)為 S2、S5、S6，隨便選擇狀態(tài) S2進行更深層的搜索[6]，直到到達狀態(tài) S15，它不響應任何相關事件，所以回來遍歷狀態(tài)S29后，會產生由事件“tkevexit”引發(fā)狀態(tài) S42。 狀態(tài) S42是一個錯誤狀態(tài)，因為它違背了安全屬性（即當一個火車經過道口時，大門是開著的），一旦狀態(tài)搜索終止，反例和錯誤軌跡就能產生(如圖4)，產生反例的路徑長度為6。同理如果遍歷S29后又遍歷S45，也會違背安全屬性，也會產生路徑長度為6的反例。

3 結果及討論

3.1 GRC模型的改進

圖4中的錯誤軌跡描繪出欄桿打開時，當一個火車穿過RC時就會導致錯誤的狀態(tài)，模型中的這個漏洞可以通過保證占用期間沒有火車后才允許欄桿打開的情況下予以避免[7]，對象欄桿的正確的UML狀態(tài)圖。將全局變量“train count”加進了模型中，它當每次火車進入道口時遞增，火車離開道口時遞減。

3.2 算法的執(zhí)行

通過在狀態(tài)搜索期間減少遍歷狀態(tài)數量方面驗證該算法，在帶有6個狀態(tài)的GRC的UML狀態(tài)模型中，由每個對象的狀態(tài)圖組合成相關事件集構成的狀態(tài)空間后，即狀態(tài)空間中僅由19個狀態(tài)組成，在檢測違反安全屬性方面，將基于相關事件的算法應用到GRC系統(tǒng)后，只搜索遍歷整個狀態(tài)空間的41%，狀態(tài)空間大大減少，并產生長度為6的反例（見表2）。

表2 算法的執(zhí)行

[1]周清雷,姬莉霞,王艷梅.基于UPPAAL的實時系統(tǒng)模型驗證[J].計算機應用,2004，24(09):129-131.

[2]李勇,李宣東,鄭國梁.實時系統(tǒng)時段性質的模型檢驗[J].計算機科學,2002，29(11):165-167.

[3]徐雨波,晏榮杰.一種基于有限精度時間自動機的模型檢測工具[J].計算機應用研究,2006(05):121-125.

[4]LANGE E.The degree of realism of gis-based virtual landscapes:Implications for spatial planning[C].In:D.Fritsch and R.S piller(eds),Photogrammertric Week’99,Herbert Wichmann Verlag,Heidelberg,1999:367-374.

[5]HENZINGER T A,JHALA R,MAJUMDAR R,et al.Software verification with blast[C].in Proc.of 10th SPIN Workshop on Model Checking Software(SPIN),LNCS 2648.Springer-Verlag,2003:235-239.

[6]BEER I,BEN-DAVID S,EISNER C,et al.Rulebase-an industryoriented formal verification tool[C].in Proc.of 33rd Design Automation Conference(DAC).Asociation for Computing Machinery,1996:655-660.

[7]MIKK E,LAKHNECH Y,HOLZMANN G,et al.Implementing statecharts in promela/spin[C].in Proc.of 2nd IEEE workshop on industrial strength formal specification techniques WIFT’98,1998:90-101.