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

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

2.1 狀態(tài)空間的構(gòu)建
    對(duì)象鐵軌有兩個(gè)正交狀態(tài)Track1和Track2。對(duì)象欄桿有4個(gè)局部狀態(tài)，Track1有5個(gè)局部狀態(tài)，Track2有5個(gè)局部狀態(tài)。GRC系統(tǒng)的U包括（4×5×5）100個(gè)狀態(tài)。通常模型限定可到達(dá)狀態(tài)的數(shù)量。表1顯示了所有可能的狀態(tài)。

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

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

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