基于事件集的反應系統模型的驗證

張 磊，馬光勝

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

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

1 提出的驗證技術

1.1 假設

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

1.2 基于事件的驗證方法

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

本節中描述的算法[2]如下：

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

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

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

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

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

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

2 實例研究

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

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

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

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

(2)GRC的UML狀態圖模型

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

2.1 狀態空間的構建

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

表1 所有可能的狀態

2.2 基于事件的算法應用到火車道口系統

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

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

3 結果及討論

3.1 GRC模型的改進

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

3.2 算法的執行

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

表2 算法的執行

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

[2]李勇,李宣東,鄭國梁.實時系統時段性質的模型檢驗[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.