摘   要： 在總結(jié)前人工作的基礎(chǔ)上，提出了一種有效檢測并發(fā)或反應(yīng)系統(tǒng)的動態(tài)行為模型中違反安全屬性的方法,目的是減少為檢測違反安全屬性所需檢測的狀態(tài)數(shù)量，驗證過程包括構(gòu)造一個由所有獨立狀態(tài)圖組成的全局狀態(tài)空間圖,并遍歷這個全局狀態(tài)空間圖中的狀態(tài)以便檢測安全協(xié)議。首先讀待驗證的安全屬性和可能會違反這些屬性的相關(guān)事件集，構(gòu)造全局狀態(tài)空間圖只考慮相關(guān)事件產(chǎn)生的狀態(tài)轉(zhuǎn)換。使用該方法驗證了“火車道口”系統(tǒng)，減少了59%的搜索空間。
關(guān)鍵詞： 反應(yīng)系統(tǒng)； 安全屬性； UML狀態(tài)空間圖； 相關(guān)事件集； 狀態(tài)轉(zhuǎn)換

    本文在沒有其他模型檢測工具的情況下使用UML狀態(tài)圖驗證已建模的反應(yīng)系統(tǒng)。反應(yīng)系統(tǒng)在這里認(rèn)為是面向狀態(tài)并對外部或內(nèi)部行動做出反應(yīng)，反應(yīng)有可能產(chǎn)生狀態(tài)或行為的變化，一個反應(yīng)系統(tǒng)（事件驅(qū)動）的行為由一系列的狀態(tài)、事件和行為集所規(guī)范。
1 提出的驗證技術(shù)
1.1 假設(shè)
    假定正在考慮中的系統(tǒng)有多個合作的對象，這些對象通過事件相互聯(lián)系。每個對象的動態(tài)行為都用UML狀態(tài)圖建模。這些對象在接收一個正確的外部或內(nèi)部產(chǎn)生事件及相應(yīng)的保護條件變?yōu)檎鎸崰顟B(tài)發(fā)生改變。要驗證的屬性用時態(tài)邏輯表示并由符號?準(zhǔn)代表。驗證過程包括每個UML狀態(tài)圖到一個元組{Si,Ei,Ti,Ii}形式的轉(zhuǎn)換。其中i代表對象，Si代表非空有限的狀態(tài)集，Ei代表事件集，Ti?哿Si×Si是一套轉(zhuǎn)換集。Ii?哿Si是一套初始狀態(tài)集。讓Et為總的事件集即Et={E1∪E2…En},其中n是系統(tǒng)對象的數(shù)量[1]。
1.2 基于事件的驗證方法
    一旦在Et中所有事件都發(fā)生時就合并所有對象的狀態(tài)轉(zhuǎn)換來建造系統(tǒng)的狀態(tài)空間,在狀態(tài)空間(on the fly)的狀態(tài)圖中找到表示為┐φ的錯誤狀態(tài)(否定行為),如果終止了更深層的狀態(tài)空間的搜索，就會演示出錯誤軌跡（反例）。
    本節(jié)中描述的算法[2]如下：
    (1)一個事件是相關(guān)的如果：
    ①存在著一個與這個事件相關(guān)的轉(zhuǎn)換并且當(dāng)前狀態(tài)是一個錯誤狀態(tài)（┐φ）
    ②存在于一個與這個事件相關(guān)的轉(zhuǎn)換并且下一個狀態(tài)為一個錯誤狀態(tài)（┐φ）
    (2)一套事件是相關(guān)的如果：
    存在著一套與這些事件相關(guān)的轉(zhuǎn)換，并且能將對象從最初狀態(tài)轉(zhuǎn)到錯誤狀態(tài)（┐φ）。即將對象從一個對象的最初狀態(tài)轉(zhuǎn)到錯誤狀態(tài)的事件集合叫做相關(guān)的事件集。
    相關(guān)事件集計算完，每個對象的UML狀態(tài)圖都轉(zhuǎn)換成這種元組{Si, Eri, Ti, Ii}，其中Eri代表聯(lián)系對象Oi的相關(guān)事件集，Ert代表總的相關(guān)事件集,即Ert={Er1∪Er2∪…Ern}。搜索狀態(tài)空間只考慮在總的相關(guān)事件集Ert中的事件。一旦到達了錯誤狀態(tài)或訪問了所有的狀態(tài)，就終止搜索狀態(tài)圖。
2 實例研究
    (1)火車道口問題是實時系統(tǒng)中的一個典型問題?；疖嚨揽谙到y(tǒng)用來操縱道口的欄桿。對于兩個鐵軌上的門位于區(qū)域A上，火車在兩個鐵軌（T1,T2）上任意方向運行[3]。圖1中顯示了已經(jīng)定位的傳感器(S1,S2,S3,S4和S5)。傳感器表明當(dāng)火車行駛到區(qū)域A、進入RC、離開區(qū)域A或退出RC。傳感器S5表明門是關(guān)著的還是開著的。“占用期間”指RC上有一個或更多火車的時期。系統(tǒng)被期望滿足如下的屬性：
    ①道口在所有占用期間是關(guān)閉的(安全)；
    ②如果占用期間沒有火車,道口是開放的(實用性)；
    ③道口在盡可能的時間里是開放的(活性)。

2.1 狀態(tài)空間的構(gòu)建
    對象鐵軌有兩個正交狀態(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)的數(shù)量。表1顯示了所有可能的狀態(tài)。

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

    在GRC模型中要檢測的安全屬性“當(dāng)火車在Track1或Track2上的RC時，道口始終關(guān)閉”[5]，時態(tài)邏輯表示為：(T1.Crossing∨T2.Crossing)?圯G.Closed，如果成立則此模型有漏洞，產(chǎn)生一個反例/錯誤軌跡[3]，否定形式表示為：(T1.Crossing∨T2.Crossing)?圯┐(G.Closed)，這就意味著火車通過時大門開著或正開著或正關(guān)閉的狀態(tài)中。
    圖3中，狀態(tài)搜索從最初狀態(tài)S1開始，由事件“tkevarrive”引發(fā)的后續(xù)狀態(tài)為 S2、S5、S6，隨便選擇狀態(tài)S2進行更深層的搜索[6]，直到到達狀態(tài)S15，它不響應(yīng)任何相關(guān)事件，所以回來遍歷狀態(tài)S29后，會產(chǎn)生由事件“tkevexit”引發(fā)狀態(tài)S42。狀態(tài)S42是一個錯誤狀態(tài)，因為它違背了安全屬性（即當(dāng)一個火車經(jīng)過道口時，大門是開著的），一旦狀態(tài)搜索終止，反例和錯誤軌跡就能產(chǎn)生(如圖4)，產(chǎn)生反例的路徑長度為6。同理如果遍歷S29后又遍歷S45，也會違背安全屬性，也會產(chǎn)生路徑長度為6的反例。

3 結(jié)果及討論
3.1 GRC模型的改進
    圖4中的錯誤軌跡描繪出欄桿打開時，當(dāng)一個火車穿過RC時就會導(dǎo)致錯誤的狀態(tài)，模型中的這個漏洞可以通過保證占用期間沒有火車后才允許欄桿打開的情況下予以避免[7]，對象欄桿的正確的UML狀態(tài)圖。將全局變量“train count”加進了模型中，它當(dāng)每次火車進入道口時遞增，火車離開道口時遞減。
3.2 算法的執(zhí)行
    通過在狀態(tài)搜索期間減少遍歷狀態(tài)數(shù)量方面驗證該算法，在帶有6個狀態(tài)的GRC的UML狀態(tài)模型中，由每個對象的狀態(tài)圖組合成相關(guān)事件集構(gòu)成的狀態(tài)空間后，即狀態(tài)空間中僅由19個狀態(tài)組成，在檢測違反安全屬性方面，將基于相關(guān)事件的算法應(yīng)用到GRC系統(tǒng)后，只搜索遍歷整個狀態(tài)空間的41%，狀態(tài)空間大大減少，并產(chǎn)生長度為6的反例（見表2）。
參考文獻
[1] 周清雷,姬莉霞,王艷梅. 基于UPPAAL的實時系統(tǒng)模型驗證[J]. 計算機應(yīng)用, 2004，24(09):129-131.
[2] 李勇,李宣東,鄭國梁.實時系統(tǒng)時段性質(zhì)的模型檢驗[J].計算機科學(xué),2002，29(11):165-167.
[3] 徐雨波, 晏榮杰. 一種基于有限精度時間自動機的模型檢測工具[J]. 計算機應(yīng)用研究, 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.