基于符號模型檢測的Web服務組合形式化驗證?

張世杰 徐 鵬 劉沛瑤

（1.西南交通大學數學學院 成都 610031）

（2.系統可信性自動驗證國家地方聯合工程實驗室 成都 610031）

1 引言

面向服務的體系結構SOA（Service Oriented Architecture）是一種構建分布式系統的方式，將功能作為服務提供，強調交互服務之間的松散耦合［1］。Web服務隨著SOA的提出而不斷發展，其是SOA體系結構的基本單元，是一種新型的Web應用［2］。隨著經濟的發展與用戶需求的多樣化和綜合化，單一Web服務所提供的功能已經不能滿足需求，因此產生了Web服務組合（Web Service Composition，WSC）。WSC可以集成現有的異構服務而組合成可以提供更復雜功能的新服務，實現更高的服務可重用性和獲取增值服務［3］。但WSC也帶來了一些新的挑戰：如何保證Web服務組合過程的正確性？如何驗證組合服務滿足某些需要的特性？如何對WSC進行有效的建模、分析和驗證？

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

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

基于窮盡搜索的模型檢測驗證方法自動化程度很高、驗證速度快、效率高、適用于Web服務數量比較多的組合服務，并且如果一個性質不滿足時會給出一個反例，有利于改進組合Web服務。該方法的難點在于如何將現實的服務組合系統轉化為對應的數學模型。Babin等［10］提出一種基于Event-B進行細化的新穎的正確構造形式方法，解決了Web服務補償的功能正確性問題。文獻［11］提出了將BPEL定義的服務組合轉化為UPPAAL模型進行自動驗證的方法。EL KASSMI等［12］使用FSM（有限狀態機）對某些安全需求進行建模，使用模型檢測工具UPPAAL驗證Web服務組合中的形式化和集成方法。周女琪等［13］將Web服務組合過程建立為定量多目標馬爾可夫決策過程，并將該模型轉化為PRISM模型，同時將不同的用戶需求建模為多目標時序邏輯公式，最后使用PRISM驗證。

針對Web服務組合形式化驗證問題仍存在的不足，如時間復雜度較高、狀態爆炸、建模難度較大、驗證結果不夠精確等，本文提出基于符號模型檢測的組合Web服務驗證方法。該方法能夠緩解狀態爆炸問題從而驗證比較復雜且服務數量較多的組合Web服務，易于構建形式化模型且可根據反例改進模型。具體工作為將Web服務實例轉換為基于消息會話的有限狀態自動機模型，通過狀態遷移圖構建形式化模型并給出時序邏輯表示的性質規約，用符號模型檢測器NuSMV自動驗證組合Web服務交互的正確性和死鎖。

2 模型檢測

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

圖1 模型檢測原理圖

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

LTL公式由原子命題、時間模態算子和邏輯連接符組成。其中時間模態算子有X（下一個狀態），G（所有未來狀態），F（某個未來狀態），U（直到），R（釋放）；邏輯連接符有：┓（否定），∧（合取），∨（析取），→（蘊涵）。LTL公式定義如下：

1）命題常量（true，false）和原子命題變元p是LTL公式；

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

3）若f，g是LTL公式，則X f，G f，F f，f U g，f R g也是LTL公式；

4）每個LTL公式都可以通過有限次數運用1）、2）、3）得到。

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

3 Web服務組合的形式化定義

Web服務組合的交互行為可以通過服務之間發送消息和接送消息改變服務內部狀態而完成，即從其他服務獲取輸入消息，經過處理后將消息發送，所以從本質上來講Web服務是一個狀態遷移系統。有限狀態自動機作為描述有限狀態遷移系統的一種抽象數學模型［15］，與基于一組狀態遷移進行表達的Web服務組合優化類似，因此使用有限狀態自動機來建模Web服務組合非常合適。基于消息會話的Web組合服務有限狀態自動機的形式化定義如下所示。

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

定義2多個Web服務交互模型的形式化定義。WM1，WM2，…，WMn是n個Web服務有限狀態自動機，它們的交互模型為n個服務的同步積自動機［16］，即

其中：S1||2||…||n=S1×S2×…×Sn是同步自動機的狀態集；

4 形式化模型

我們將Web服務的操作用有限狀態自動機消息的發送和接收表示，狀態用有限狀態自動機的狀態表示，當執行單一服務中的操作時組合Web服務的狀態將會改變。Web服務組合的基本流程有四種結構：順序組合，并發組合，選擇組合和循環組合，其有限狀態自動機分別如圖2、3、4、5所示。其中Si表示狀態，Mr和Ms分別表示接收的消息、發送的消息，WMi表示單一服務的有限狀態自動機。

圖2 Web服務組合的順序結構

圖3 Web服務組合的并發結構

圖4 Web服務組合的選擇結構

基于符號模型檢測的Web服務組合形式化驗證過程是將服務組合系統建模為一個有限狀態遷移系統模型，模型中狀態間的遷移模擬實際系統的運行，需驗證的系統性質用CTL和LTL描述，NuSMV實現形式化模型自動驗證。具體建模步驟有三步：

1）為每一個參與交互的Web服務構建有限狀態自動機。每個服務用一個有限狀態自動機表示，畫出其狀態遷移圖。集合Mr和Ms分別表示此服務與其他服務交互時的接收消息集和發送消息集。服務接收或者發送消息后狀態發生遷移，用有向箭頭上標記的接收或發送消息表示。

圖5 Web服務組合的循環結構

2）構建形式化模型。NuSMV建模語言描述1）中已畫出的狀態遷移圖，CTL和LTL描述需要驗證的性質條件。構建模型時采用模塊化結構，每一個服務（即自動機）用一個模塊表示，并且用關鍵詞process修飾。由于模型中消息集元素眾多，所以用一個布爾型數組表示，每一個數組元素對應一個接收消息或者發送消息。

3）驗證形式化模型。如果性質不滿足將會給出一個反例向用戶報告錯誤的原因，通過驗證結果，可以分析服務交互的正確性和死鎖狀態。

5 實例驗證

本文以在線圖書訂購服務（online bookshop service）為例使用符號模型檢測器NuSMV形式化驗證組合服務。該組合服務包括4個獨立的Web服務，分別是前臺服務（windows service）、書店服務（bookshop service）、出版社服務（publisher service）、托運服務（shipper service），交互過程如圖6所示。

圖6 在線圖書訂購服務

當前臺服務接收到購買者的訂單請求后，向書店服務發送一個訂單消息order，書店服務收到該消息后，檢索出圖書的編碼號isbn，并通過發送一個查詢消息query，通知出版社服務向購買者發送圖書；出版社服務收到該消息后會發送一個存貨消息inventory，告知書店服務目前該書的庫存情況；書店服務收到inventory消息后會向前臺服務發送一個賬單消息bill，而前臺服務在接收到該消息后會通知購買者支付賬單并發送一個賬單處理消息handbill；出版社服務在接收到該消息后向托運服務發送請求托運消息consign，通知其向購買者運送該圖書；而托運服務會返回確認消息notify。

5.1 構建有限狀態自動機模型

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

圖7 出版社服務（publisher service）的狀態遷移圖

圖8 前臺服務（windows service）的狀態遷移圖

圖9 書店服務（bookshop service）的狀態遷移圖

圖10 托運服務（shipper service）的狀態遷移圖

5.2 構建形式化模型

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

圖11 部分NuSMV模型

時序邏輯公式LTL和CTL表示系統的性質約束，本例判定服務組合有無死鎖狀態（失配現象）及服務組合交互過程是否正確。公式如下所示，其中有無死鎖狀態用LTL公式表示，LTLSPEC語句實現；正確性用CTL公式表示，SPEC語句實現。

1）死鎖狀態（失配現象）：LTL公式GF（（pr1.sw=w3）&（pr2.sb=b4）&（pr3.sp=p5）&（pr4.ss=s2））表示每一個服務的狀態都會到達終止狀態，若該公式為TRUE則不存在死鎖狀態。

圖12 死鎖及正確性驗證實驗結果

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））刻畫了網上圖書訂購服務的完整交互過程，通過對滿足該CTL公式的狀態進行標記，可以判斷服務組合的正確性。

5.3 驗證結果

本文構建的形式化模型的服務組建數量為4個，狀態數達到160個，符號模型檢測器NuSMV對其進行驗證未出現狀態爆炸問題，實驗結果如圖12所示。實驗結果表明驗證死鎖性質的公式為false并給出了反例，即4個服務之間存在死鎖狀態（失配現象）。由定義2得到4個服務的同步積自動機WM1||WM2||WM3||WM4，并分析實驗結果得到反例為（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）為死鎖狀態，此時WM2已經運行到終止狀態，而其余3個服務都沒有到達終止狀態。

實驗結果也表明驗證服務組合交互過程正確性的公式為false，即4個Web服務之間的交互是不正確的。分析實驗結果給出的反例對服務組合交互過程進行改進，如圖13所示在原模型中添加語句：&message［1］，即在前臺服務中當初始狀態w0遷移到狀態w1時使message［1］的值為TRUE。同樣在書店服務、出版社服務、托運服務中，初始狀態遷移到下一個狀態時使對應的消息值為TRUE，而模型其他部分不改變。

圖13 改進后的模型

驗證改進后的模型得到實驗結果如圖14所示，實驗結果表明CTL公式值為TRUE，說明4個服務之間的交互正確。由實驗結果可以得到網上圖書訂購服務的狀態遷移過程，即由4個服務的初始狀態的組合（w0，b0，p0，s0）開始，狀態遷移過程為（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），狀態（w3，b4，p5，s2）表示4個服務的終止狀態的組合。

圖14 正確性驗證實驗結果

6 結語

本文針對Web服務組合形式化驗證問題的不足，提出了基于符號模型檢測的Web服務組合形式化驗證的方法，給出了基于消息會話的Web服務有限狀態自動機的形式化定義和多個Web服務組合的有限狀態自動機的形式化定義，詳細說明了使用模型檢測驗證Web服務組合性質的過程。最后通過一個實例對死鎖狀態和交互正確性驗證，并對正確性驗證的實驗結果給出的反例進行分析，給出改進的形式化模型，得到的實驗結果說明了本文方法的可行性。實驗結果表明未出現狀態爆炸，該方法也適用于其他狀態數量較多的Web服務組合驗證。下一步將探討如何高效快速地對更復雜的Web服務組合進行形式化建模，將對其他性質進行驗證以及將本文方法與業務流程執行語言BPEL描述的Web服務組合結合。