基于符號(hào)模型檢測(cè)的Web服務(wù)組合形式化驗(yàn)證?

張世杰 徐 鵬 劉沛瑤

（1.西南交通大學(xué)數(shù)學(xué)學(xué)院 成都 610031）

（2.系統(tǒng)可信性自動(dòng)驗(yàn)證國(guó)家地方聯(lián)合工程實(shí)驗(yàn)室 成都 610031）

1 引言

面向服務(wù)的體系結(jié)構(gòu)SOA（Service Oriented Architecture）是一種構(gòu)建分布式系統(tǒng)的方式，將功能作為服務(wù)提供，強(qiáng)調(diào)交互服務(wù)之間的松散耦合［1］。Web服務(wù)隨著SOA的提出而不斷發(fā)展，其是SOA體系結(jié)構(gòu)的基本單元，是一種新型的Web應(yīng)用［2］。隨著經(jīng)濟(jì)的發(fā)展與用戶需求的多樣化和綜合化，單一Web服務(wù)所提供的功能已經(jīng)不能滿足需求，因此產(chǎn)生了Web服務(wù)組合（Web Service Composition，WSC）。WSC可以集成現(xiàn)有的異構(gòu)服務(wù)而組合成可以提供更復(fù)雜功能的新服務(wù)，實(shí)現(xiàn)更高的服務(wù)可重用性和獲取增值服務(wù)［3］。但WSC也帶來(lái)了一些新的挑戰(zhàn)：如何保證Web服務(wù)組合過(guò)程的正確性？如何驗(yàn)證組合服務(wù)滿足某些需要的特性？如何對(duì)WSC進(jìn)行有效的建模、分析和驗(yàn)證？

Web服務(wù)組合問(wèn)題包括：Web服務(wù)發(fā)現(xiàn)，Web服務(wù)組合及組合Web服務(wù)的形式化驗(yàn)證。本文研究的重點(diǎn)是組合Web服務(wù)的形式化驗(yàn)證，其是保證組合Web服務(wù)正式發(fā)布投入市場(chǎng)運(yùn)行，減小其故障的重要手段。常用的服務(wù)組合驗(yàn)證方法是69%的模型檢查，進(jìn)程代數(shù)的使用率為29%，定理證明方法應(yīng)用于9%的被調(diào)查機(jī)制。Web服務(wù)組合驗(yàn)證廣泛使用的建模工具是NuSMV（22%），SPIN（17%），CPN（12%），UPPAAL（12%），Event-B（10%）和PAT（5%）［4］。

基于Petri網(wǎng)及進(jìn)程代數(shù)的演繹驗(yàn)證方法驗(yàn)證能力很強(qiáng)，但自動(dòng)化程度不高驗(yàn)證過(guò)程需要大量人工參與，當(dāng)組合Web服務(wù)系統(tǒng)比較龐大時(shí)就變得相當(dāng)復(fù)雜。沈華等［5］在基于隨機(jī)Petri網(wǎng)的Web服務(wù)組合模型WSCPAM的基礎(chǔ)上，提出了對(duì)模型進(jìn)行有界性、死鎖、陷阱驗(yàn)證的必要性、意義和算法實(shí)現(xiàn)。倪悅等［6］提出一種語(yǔ)義Web服務(wù)組合模型到著色Petri網(wǎng)組合模型的轉(zhuǎn)換方法，給出了組合服務(wù)的語(yǔ)義一致性驗(yàn)證算法，以一個(gè)協(xié)同設(shè)計(jì)過(guò)程為例對(duì)組合服務(wù)流程進(jìn)行仿真驗(yàn)證并在工作流引擎中部署執(zhí)行。文獻(xiàn)［7］提出某種轉(zhuǎn)換規(guī)則將描述Web服務(wù)組合的BPEL文件轉(zhuǎn)化為具有直觀性的Petri圖，通過(guò)對(duì)Petri圖的相關(guān)性質(zhì)找出BPEL的不足之處。文獻(xiàn)［8］提出基于擴(kuò)展有限自動(dòng)機(jī)驗(yàn)證組合Web服務(wù)的辦法，不但可以驗(yàn)證組合Web服務(wù)是否滿足系統(tǒng)需求，還可以驗(yàn)證運(yùn)行過(guò)程是否有邏輯錯(cuò)誤。胡靜等［9］在多元Pi-演算的基礎(chǔ)上給出Web服務(wù)的描述模型、子類型關(guān)系定義和可替換性定義，并對(duì)Web服務(wù)的相容性進(jìn)行細(xì)化；基于定義給出正確性判定規(guī)則和可替換性判定方法。

基于窮盡搜索的模型檢測(cè)驗(yàn)證方法自動(dòng)化程度很高、驗(yàn)證速度快、效率高、適用于Web服務(wù)數(shù)量比較多的組合服務(wù)，并且如果一個(gè)性質(zhì)不滿足時(shí)會(huì)給出一個(gè)反例，有利于改進(jìn)組合Web服務(wù)。該方法的難點(diǎn)在于如何將現(xiàn)實(shí)的服務(wù)組合系統(tǒng)轉(zhuǎn)化為對(duì)應(yīng)的數(shù)學(xué)模型。Babin等［10］提出一種基于Event-B進(jìn)行細(xì)化的新穎的正確構(gòu)造形式方法，解決了Web服務(wù)補(bǔ)償?shù)墓δ苷_性問(wèn)題。文獻(xiàn)［11］提出了將BPEL定義的服務(wù)組合轉(zhuǎn)化為UPPAAL模型進(jìn)行自動(dòng)驗(yàn)證的方法。EL KASSMI等［12］使用FSM（有限狀態(tài)機(jī)）對(duì)某些安全需求進(jìn)行建模，使用模型檢測(cè)工具UPPAAL驗(yàn)證Web服務(wù)組合中的形式化和集成方法。周女琪等［13］將Web服務(wù)組合過(guò)程建立為定量多目標(biāo)馬爾可夫決策過(guò)程，并將該模型轉(zhuǎn)化為PRISM模型，同時(shí)將不同的用戶需求建模為多目標(biāo)時(shí)序邏輯公式，最后使用PRISM驗(yàn)證。

針對(duì)Web服務(wù)組合形式化驗(yàn)證問(wèn)題仍存在的不足，如時(shí)間復(fù)雜度較高、狀態(tài)爆炸、建模難度較大、驗(yàn)證結(jié)果不夠精確等，本文提出基于符號(hào)模型檢測(cè)的組合Web服務(wù)驗(yàn)證方法。該方法能夠緩解狀態(tài)爆炸問(wèn)題從而驗(yàn)證比較復(fù)雜且服務(wù)數(shù)量較多的組合Web服務(wù)，易于構(gòu)建形式化模型且可根據(jù)反例改進(jìn)模型。具體工作為將Web服務(wù)實(shí)例轉(zhuǎn)換為基于消息會(huì)話的有限狀態(tài)自動(dòng)機(jī)模型，通過(guò)狀態(tài)遷移圖構(gòu)建形式化模型并給出時(shí)序邏輯表示的性質(zhì)規(guī)約，用符號(hào)模型檢測(cè)器NuSMV自動(dòng)驗(yàn)證組合Web服務(wù)交互的正確性和死鎖。

2 模型檢測(cè)

模型檢測(cè)是一種通過(guò)窮盡搜索所有可能的系統(tǒng)狀態(tài)自動(dòng)檢測(cè)有限狀態(tài)系統(tǒng)是否滿足其設(shè)計(jì)規(guī)范的驗(yàn)證技術(shù)，包括兩方面：一方面將實(shí)際系統(tǒng)建模成模型檢測(cè)器能夠識(shí)別的形式化模型；另一方面用線性時(shí)序邏輯（Linear Temporal Logic，LTL）、分支時(shí)序邏輯（Computation Tree Logic，CTL）等描述系統(tǒng)的性質(zhì)。模型檢測(cè)原理如圖1所示，輸入是模型和性質(zhì)，輸出結(jié)果為TRUE時(shí)說(shuō)明性質(zhì)滿足，輸出結(jié)果為FALSE時(shí)說(shuō)明性質(zhì)不滿足并給出反例。狀態(tài)空間爆炸是制約模型檢測(cè)發(fā)展的最大問(wèn)題，減少狀態(tài)爆炸問(wèn)題的主要技術(shù)有偏序規(guī)約、抽象和對(duì)稱等，而符號(hào)模型檢測(cè)能有效緩解狀態(tài)爆炸。

圖1 模型檢測(cè)原理圖

常用的模型檢測(cè)工具有SPIN，UPPAAL，NuSMV，PRISM，其中NuSMV（New Symbolic Model Verifier）是Carnegie Mellon University（CMU）的Mc?Millan博士在SMV基礎(chǔ)上再構(gòu)造、再實(shí)現(xiàn)和擴(kuò)展的，是第一款基于BDDs（Binary Decision Diagrams）的符號(hào)模型檢測(cè)器［14］。NuSMV形式化模型是由模塊化構(gòu)成的狀態(tài)遷移系統(tǒng)，通常將實(shí)際系統(tǒng)中的每一個(gè)實(shí)體角色建模為一個(gè)模塊，但必須有一個(gè)主模塊，類似c和c++。形式化模型中VAR語(yǔ)句表示變量聲明，ASSIGN語(yǔ)句表示變量的賦值和遷移關(guān)系，SPEC語(yǔ)句表示系統(tǒng)的屬性規(guī)約。屬性規(guī)約可以由時(shí)序邏輯公式（LTL和CTL）、不變表達(dá)式（invariant expression）以及能夠計(jì)算從一個(gè)指定狀態(tài)到另一個(gè)指定狀態(tài)的最小或最大路徑的表達(dá)式表示。

LTL公式由原子命題、時(shí)間模態(tài)算子和邏輯連接符組成。其中時(shí)間模態(tài)算子有X（下一個(gè)狀態(tài)），G（所有未來(lái)狀態(tài)），F(xiàn)（某個(gè)未來(lái)狀態(tài)），U（直到），R（釋放）；邏輯連接符有：┓（否定），∧（合?。?，∨（析取），→（蘊(yùn)涵）。LTL公式定義如下：

1）命題常量（true，false）和原子命題變?cè)猵是LTL公式；

2）若f，g是LTL公式，則┓f，f ∧g，f ∨g，f →g也是LTL公式；

3）若f，g是LTL公式，則X f，G f，F(xiàn) f，f U g，f R g也是LTL公式；

4）每個(gè)LTL公式都可以通過(guò)有限次數(shù)運(yùn)用1）、2）、3）得到。

CTL公式由一對(duì)操作符表示，第一個(gè)操作符是路徑量詞A（對(duì)所有的路徑）或E（存在一個(gè)路徑）；第二個(gè)操作符是時(shí)態(tài)運(yùn)算符，包括G（global）、F（fi?nal）、X（next）和U（untill）。例如，AG（f）表示公式f在所有路徑的所有狀態(tài)都滿足，即f總是滿足的；EF（f）表示存在一個(gè)路徑的某個(gè)狀態(tài)使得f滿足。

3 Web服務(wù)組合的形式化定義

Web服務(wù)組合的交互行為可以通過(guò)服務(wù)之間發(fā)送消息和接送消息改變服務(wù)內(nèi)部狀態(tài)而完成，即從其他服務(wù)獲取輸入消息，經(jīng)過(guò)處理后將消息發(fā)送，所以從本質(zhì)上來(lái)講Web服務(wù)是一個(gè)狀態(tài)遷移系統(tǒng)。有限狀態(tài)自動(dòng)機(jī)作為描述有限狀態(tài)遷移系統(tǒng)的一種抽象數(shù)學(xué)模型［15］，與基于一組狀態(tài)遷移進(jìn)行表達(dá)的Web服務(wù)組合優(yōu)化類似，因此使用有限狀態(tài)自動(dòng)機(jī)來(lái)建模Web服務(wù)組合非常合適。基于消息會(huì)話的Web組合服務(wù)有限狀態(tài)自動(dòng)機(jī)的形式化定義如下所示。

定義1Web服務(wù)有限狀態(tài)自動(dòng)機(jī)。滿足下列條件的一個(gè)六元組WM=＜S，s0，F(xiàn)，Mr，Ms，δ＞稱為Web服務(wù)有限狀態(tài)自動(dòng)機(jī)，其中：S=＜s0，s1，s2，…，sn＞是非空有限狀態(tài)集，?si∈S稱為WM的一個(gè)狀態(tài)；s0∈S是初始狀態(tài)；F ?S是終止?fàn)顟B(tài)集，?si∈F稱為終止?fàn)顟B(tài)；Mr={mr1,mr2,…,mrn}是非空有限接收消息集；MS={mS1,mS2,…,mSn} 是非空有限發(fā)送消息集；δ:S×Mr→S或δ:S×MS→S稱為狀態(tài)遷移函數(shù)，即(s,mr)∈S×Mr有δ(s,mr)=s′，表示W(wǎng)eb服務(wù)有限狀態(tài)自動(dòng)機(jī)WM在狀態(tài)s接收消息后狀態(tài)遷移到s′，(s,mS)∈S×MS有δ(s,mS)=s′，表示W(wǎng)M在狀態(tài)s發(fā)送消息后將狀態(tài)遷移到s′。

定義2多個(gè)Web服務(wù)交互模型的形式化定義。WM1，WM2，…，WMn是n個(gè)Web服務(wù)有限狀態(tài)自動(dòng)機(jī)，它們的交互模型為n個(gè)服務(wù)的同步積自動(dòng)機(jī)［16］，即

其中：S1||2||…||n=S1×S2×…×Sn是同步自動(dòng)機(jī)的狀態(tài)集；

4 形式化模型

我們將Web服務(wù)的操作用有限狀態(tài)自動(dòng)機(jī)消息的發(fā)送和接收表示，狀態(tài)用有限狀態(tài)自動(dòng)機(jī)的狀態(tài)表示，當(dāng)執(zhí)行單一服務(wù)中的操作時(shí)組合Web服務(wù)的狀態(tài)將會(huì)改變。Web服務(wù)組合的基本流程有四種結(jié)構(gòu)：順序組合，并發(fā)組合，選擇組合和循環(huán)組合，其有限狀態(tài)自動(dòng)機(jī)分別如圖2、3、4、5所示。其中Si表示狀態(tài)，Mr和Ms分別表示接收的消息、發(fā)送的消息，WMi表示單一服務(wù)的有限狀態(tài)自動(dòng)機(jī)。

圖2 Web服務(wù)組合的順序結(jié)構(gòu)

圖3 Web服務(wù)組合的并發(fā)結(jié)構(gòu)

圖4 Web服務(wù)組合的選擇結(jié)構(gòu)

基于符號(hào)模型檢測(cè)的Web服務(wù)組合形式化驗(yàn)證過(guò)程是將服務(wù)組合系統(tǒng)建模為一個(gè)有限狀態(tài)遷移系統(tǒng)模型，模型中狀態(tài)間的遷移模擬實(shí)際系統(tǒng)的運(yùn)行，需驗(yàn)證的系統(tǒng)性質(zhì)用CTL和LTL描述，NuSMV實(shí)現(xiàn)形式化模型自動(dòng)驗(yàn)證。具體建模步驟有三步：

1）為每一個(gè)參與交互的Web服務(wù)構(gòu)建有限狀態(tài)自動(dòng)機(jī)。每個(gè)服務(wù)用一個(gè)有限狀態(tài)自動(dòng)機(jī)表示，畫出其狀態(tài)遷移圖。集合Mr和Ms分別表示此服務(wù)與其他服務(wù)交互時(shí)的接收消息集和發(fā)送消息集。服務(wù)接收或者發(fā)送消息后狀態(tài)發(fā)生遷移，用有向箭頭上標(biāo)記的接收或發(fā)送消息表示。

圖5 Web服務(wù)組合的循環(huán)結(jié)構(gòu)

2）構(gòu)建形式化模型。NuSMV建模語(yǔ)言描述1）中已畫出的狀態(tài)遷移圖，CTL和LTL描述需要驗(yàn)證的性質(zhì)條件。構(gòu)建模型時(shí)采用模塊化結(jié)構(gòu)，每一個(gè)服務(wù)（即自動(dòng)機(jī)）用一個(gè)模塊表示，并且用關(guān)鍵詞process修飾。由于模型中消息集元素眾多，所以用一個(gè)布爾型數(shù)組表示，每一個(gè)數(shù)組元素對(duì)應(yīng)一個(gè)接收消息或者發(fā)送消息。

3）驗(yàn)證形式化模型。如果性質(zhì)不滿足將會(huì)給出一個(gè)反例向用戶報(bào)告錯(cuò)誤的原因，通過(guò)驗(yàn)證結(jié)果，可以分析服務(wù)交互的正確性和死鎖狀態(tài)。

5 實(shí)例驗(yàn)證

本文以在線圖書訂購(gòu)服務(wù)（online bookshop service）為例使用符號(hào)模型檢測(cè)器NuSMV形式化驗(yàn)證組合服務(wù)。該組合服務(wù)包括4個(gè)獨(dú)立的Web服務(wù)，分別是前臺(tái)服務(wù)（windows service）、書店服務(wù)（bookshop service）、出版社服務(wù)（publisher service）、托運(yùn)服務(wù)（shipper service），交互過(guò)程如圖6所示。

圖6 在線圖書訂購(gòu)服務(wù)

當(dāng)前臺(tái)服務(wù)接收到購(gòu)買者的訂單請(qǐng)求后，向書店服務(wù)發(fā)送一個(gè)訂單消息order，書店服務(wù)收到該消息后，檢索出圖書的編碼號(hào)isbn，并通過(guò)發(fā)送一個(gè)查詢消息query，通知出版社服務(wù)向購(gòu)買者發(fā)送圖書；出版社服務(wù)收到該消息后會(huì)發(fā)送一個(gè)存貨消息inventory，告知書店服務(wù)目前該書的庫(kù)存情況；書店服務(wù)收到inventory消息后會(huì)向前臺(tái)服務(wù)發(fā)送一個(gè)賬單消息bill，而前臺(tái)服務(wù)在接收到該消息后會(huì)通知購(gòu)買者支付賬單并發(fā)送一個(gè)賬單處理消息handbill；出版社服務(wù)在接收到該消息后向托運(yùn)服務(wù)發(fā)送請(qǐng)求托運(yùn)消息consign，通知其向購(gòu)買者運(yùn)送該圖書；而托運(yùn)服務(wù)會(huì)返回確認(rèn)消息notify。

5.1 構(gòu)建有限狀態(tài)自動(dòng)機(jī)模型

根據(jù)在線圖書訂購(gòu)服務(wù)的交互描述及定義1構(gòu)建每個(gè)Web服務(wù)的有限狀態(tài)自動(dòng)機(jī)模型，分別用WM1表示前臺(tái)服務(wù)，WM2表示書店服務(wù)，WM3表示出版社服務(wù)，WM4表示托運(yùn)服務(wù)。以出版社服務(wù)為例，其有限狀態(tài)自動(dòng)機(jī)WM3=＜S,s0,F,Mr,Ms,δ＞，其中：有限狀態(tài)集S={p0，p1，p2，p3，p4，p5}有6個(gè)狀態(tài)；s0=p0為初始狀態(tài)；F=p5為終止?fàn)顟B(tài)；接收消息集Mr=｛query，handbill，notify｝，發(fā)送消息集Ms=｛inventory，consign｝；狀態(tài)遷移函數(shù)δ={{p0,query,p1},{p1,inventory,p2},{p2,handbill,p3},{p3,consign,p4},{p4,notify,p5}}。圖7為出版社服務(wù)的狀態(tài)遷移圖，P0表示初始狀態(tài)，帶方向的箭頭指向初始狀態(tài)，終止?fàn)顟B(tài)P5用環(huán)形圈表示，有向箭頭表示狀態(tài)遷移，箭頭上標(biāo)記的消息（？代表接收消息，！代表發(fā)送消息）表示狀態(tài)遷移的條件。同樣的方法給出前臺(tái)服務(wù)、書店服務(wù)、托運(yùn)服務(wù)的狀態(tài)遷移圖，如圖8、圖9、圖10所示。

圖7 出版社服務(wù)（publisher service）的狀態(tài)遷移圖

圖8 前臺(tái)服務(wù)（windows service）的狀態(tài)遷移圖

圖9 書店服務(wù)（bookshop service）的狀態(tài)遷移圖

圖10 托運(yùn)服務(wù)（shipper service）的狀態(tài)遷移圖

5.2 構(gòu)建形式化模型

根據(jù)狀態(tài)遷移圖構(gòu)建網(wǎng)上圖書訂購(gòu)服務(wù)的形式化模型，如圖11所示。形式化模型由5個(gè)模塊構(gòu)成，包括1個(gè)主模塊和4個(gè)子模塊。4個(gè)子模塊分別對(duì)應(yīng)前臺(tái)服務(wù)、書店服務(wù)、出版社服務(wù)和托運(yùn)服務(wù)，前面使用process關(guān)鍵詞，使得模塊異步合成。模型中以“--”開頭的為注釋語(yǔ)句表示本例中的消息數(shù)組，每一個(gè)數(shù)組元素都是布爾類型且對(duì)應(yīng)一個(gè)消息，如message［1］對(duì)應(yīng)訂單消息order，數(shù)組元素初始值為FALSE，當(dāng)消息被發(fā)送時(shí)值變?yōu)門RUE。sw表示前臺(tái)服務(wù)的狀態(tài)集，包括4個(gè)狀態(tài)分別為w0，w1，w2，w3；sb表示書店服務(wù)的狀態(tài)集，包括5個(gè)狀態(tài)分別為b0，b1，b2，b3，b4；sp表示出版社服務(wù)的狀態(tài)集，包括6個(gè)狀態(tài)分別為p0，p1，p2，p3，p4，p5；ss表示托運(yùn)服務(wù)的狀態(tài)集，包括3個(gè)狀態(tài)分別為s0，s1，s2。狀態(tài)的遷移通過(guò)消息的接收和發(fā)送實(shí)現(xiàn)，狀態(tài)值及消息值的變化由ASSIGN語(yǔ)句實(shí)現(xiàn)。

圖11 部分NuSMV模型

時(shí)序邏輯公式LTL和CTL表示系統(tǒng)的性質(zhì)約束，本例判定服務(wù)組合有無(wú)死鎖狀態(tài)（失配現(xiàn)象）及服務(wù)組合交互過(guò)程是否正確。公式如下所示，其中有無(wú)死鎖狀態(tài)用LTL公式表示，LTLSPEC語(yǔ)句實(shí)現(xiàn)；正確性用CTL公式表示，SPEC語(yǔ)句實(shí)現(xiàn)。

1）死鎖狀態(tài)（失配現(xiàn)象）：LTL公式GF（（pr1.sw=w3）&（pr2.sb=b4）&（pr3.sp=p5）&（pr4.ss=s2））表示每一個(gè)服務(wù)的狀態(tài)都會(huì)到達(dá)終止?fàn)顟B(tài)，若該公式為TRUE則不存在死鎖狀態(tài)。

圖12 死鎖及正確性驗(yàn)證實(shí)驗(yàn)結(jié)果

2）正確性：CTL公式AG（（pr1.sw=w1-＞AX pr2.sb=b0）&（pr2.sb=b1-＞AX pr2.sb=b2）&（pr2.sb=b2-＞ AX pr3.sp=p0）&（pr3.sp=p1-＞ AX pr3.sp=p2）&（pr3.sp=p2-＞AX pr2.sb=b2）&（pr2.sb=b3-＞AX pr2.sb=b4）&（pr2.sb=b4-＞AX pr1.sw=w1）&（pr1.sw=w2-＞AX pr1.sw=w3）&（pr1.sw=w3-＞AX pr3.sp=p2）&（pr3.sp=p3-＞AX pr3.sp=p4）&（pr3.sp=p4-＞AX pr4.ss=s0）&（pr4.ss=s1-＞AX pr4.ss=s2）&（pr4.ss=s2-＞AX pr3.sp=p4）&（pr3.sp=p4-＞AX pr3.sp=p5））刻畫了網(wǎng)上圖書訂購(gòu)服務(wù)的完整交互過(guò)程，通過(guò)對(duì)滿足該CTL公式的狀態(tài)進(jìn)行標(biāo)記，可以判斷服務(wù)組合的正確性。

5.3 驗(yàn)證結(jié)果

本文構(gòu)建的形式化模型的服務(wù)組建數(shù)量為4個(gè)，狀態(tài)數(shù)達(dá)到160個(gè)，符號(hào)模型檢測(cè)器NuSMV對(duì)其進(jìn)行驗(yàn)證未出現(xiàn)狀態(tài)爆炸問(wèn)題，實(shí)驗(yàn)結(jié)果如圖12所示。實(shí)驗(yàn)結(jié)果表明驗(yàn)證死鎖性質(zhì)的公式為false并給出了反例，即4個(gè)服務(wù)之間存在死鎖狀態(tài)（失配現(xiàn)象）。由定義2得到4個(gè)服務(wù)的同步積自動(dòng)機(jī)WM1||WM2||WM3||WM4，并分析實(shí)驗(yàn)結(jié)果得到反例為（w0，b0，p0，s0），（w1，b0，p0，s0），（w1，b1，p0，s0），（w1，b2，p1，s0），（w1，b2，p2，s0），（w1，b3，p2，s0），（w1，b4，p2，s0）。（w1，b4，p2，s0）為死鎖狀態(tài)，此時(shí)WM2已經(jīng)運(yùn)行到終止?fàn)顟B(tài)，而其余3個(gè)服務(wù)都沒(méi)有到達(dá)終止?fàn)顟B(tài)。

實(shí)驗(yàn)結(jié)果也表明驗(yàn)證服務(wù)組合交互過(guò)程正確性的公式為false，即4個(gè)Web服務(wù)之間的交互是不正確的。分析實(shí)驗(yàn)結(jié)果給出的反例對(duì)服務(wù)組合交互過(guò)程進(jìn)行改進(jìn)，如圖13所示在原模型中添加語(yǔ)句：&message［1］，即在前臺(tái)服務(wù)中當(dāng)初始狀態(tài)w0遷移到狀態(tài)w1時(shí)使message［1］的值為TRUE。同樣在書店服務(wù)、出版社服務(wù)、托運(yùn)服務(wù)中，初始狀態(tài)遷移到下一個(gè)狀態(tài)時(shí)使對(duì)應(yīng)的消息值為TRUE，而模型其他部分不改變。

圖13 改進(jìn)后的模型

驗(yàn)證改進(jìn)后的模型得到實(shí)驗(yàn)結(jié)果如圖14所示，實(shí)驗(yàn)結(jié)果表明CTL公式值為TRUE，說(shuō)明4個(gè)服務(wù)之間的交互正確。由實(shí)驗(yàn)結(jié)果可以得到網(wǎng)上圖書訂購(gòu)服務(wù)的狀態(tài)遷移過(guò)程，即由4個(gè)服務(wù)的初始狀態(tài)的組合（w0，b0，p0，s0）開始，狀態(tài)遷移過(guò)程為（w1，b0，p0，s0），（w1，b1，p0，s0），（w1，b2，p0，s0），（w1，b2，p1，s0），（w1，b2，p2，s0），（w1，b3，p2，s0），（w1，b4，p2，s0），（w2，b4，p2，s0），（w3，b4，p2，s0），（w3，b4，p3，s0），（w3，b4，p4，s0），（w3，b4，p4，s1），（w3，b4，p4，s2），（w3，b4，p5，s2），狀態(tài)（w3，b4，p5，s2）表示4個(gè)服務(wù)的終止?fàn)顟B(tài)的組合。

圖14 正確性驗(yàn)證實(shí)驗(yàn)結(jié)果

6 結(jié)語(yǔ)

本文針對(duì)Web服務(wù)組合形式化驗(yàn)證問(wèn)題的不足，提出了基于符號(hào)模型檢測(cè)的Web服務(wù)組合形式化驗(yàn)證的方法，給出了基于消息會(huì)話的Web服務(wù)有限狀態(tài)自動(dòng)機(jī)的形式化定義和多個(gè)Web服務(wù)組合的有限狀態(tài)自動(dòng)機(jī)的形式化定義，詳細(xì)說(shuō)明了使用模型檢測(cè)驗(yàn)證Web服務(wù)組合性質(zhì)的過(guò)程。最后通過(guò)一個(gè)實(shí)例對(duì)死鎖狀態(tài)和交互正確性驗(yàn)證，并對(duì)正確性驗(yàn)證的實(shí)驗(yàn)結(jié)果給出的反例進(jìn)行分析，給出改進(jìn)的形式化模型，得到的實(shí)驗(yàn)結(jié)果說(shuō)明了本文方法的可行性。實(shí)驗(yàn)結(jié)果表明未出現(xiàn)狀態(tài)爆炸，該方法也適用于其他狀態(tài)數(shù)量較多的Web服務(wù)組合驗(yàn)證。下一步將探討如何高效快速地對(duì)更復(fù)雜的Web服務(wù)組合進(jìn)行形式化建模，將對(duì)其他性質(zhì)進(jìn)行驗(yàn)證以及將本文方法與業(yè)務(wù)流程執(zhí)行語(yǔ)言BPEL描述的Web服務(wù)組合結(jié)合。