一種驗(yàn)證Ｗｅｂ服務(wù)流程的新方法

（東南大學(xué) 計(jì)算機(jī)學(xué)院，南京 210096）



摘 要：

在實(shí)際的服務(wù)組合中，Web服務(wù)流程（process）的驗(yàn)證(verification)對(duì)于Web服務(wù)的組合實(shí)現(xiàn)和應(yīng)用具有重要意義——通過驗(yàn)證可以證明一個(gè)組合服務(wù)的控制流滿足某個(gè)重要或者期望的屬性，如不包含死鎖或不包含無限循環(huán)，諸如此類；而服務(wù)提供者可對(duì)Web服務(wù)流程進(jìn)行驗(yàn)證，以確保所提供的Web服務(wù)是完全正確的。然而，針對(duì)這兩種語言的驗(yàn)證方法較少被人們注意。提出一種驗(yàn)證Web服務(wù)流程的方法，該方法使用時(shí)序行為邏輯（TLA）建模服務(wù)流程，然后，利用模型檢驗(yàn)（model checking）技術(shù)驗(yàn)證模型的某些屬性。實(shí)驗(yàn)證明該方法效果良好，有相當(dāng)?shù)奶剿髋c實(shí)用價(jià)值。

關(guān)鍵詞：時(shí)序邏輯語言； Web服務(wù)本體描述語言； Web服務(wù)業(yè)務(wù)流程執(zhí)行語言； Web服務(wù)組合驗(yàn)證； 工作流模型分析

中圖分類號(hào)：TP311 文獻(xiàn)標(biāo)志碼：A

文章編號(hào)：10013695(2008)12378505



Novel method to verify Web services process



WANG Chen， WANG Hongbing， XU Xun

（School of Computer Science Engineering， Southeast University， Nanjing 210096， China）



Abstract:OWLS and BPEL4WS are two widely used services description language which applied in modeling and implementing service composition. In the real services composition， the verification of Web services process plays an important role. Through the verification， the paper proved that a control flow of the services composition could satisfy some important or expected properties， some key properties such as no deadlock， no infinite loop and so on; also the service provider may verify Web services process to ensure that the Web services which they provided were completely correct. However， little attention had been paid to the methods which verify these two description language. And proposed a verification method of Web services which used TLA to model the services process， and then used the technology， model checking to verify some key properties. Through experiments， proves that it has good effect and is a potential and useful method in real environment.

Key words：temporal logic of action; ontology Web language for services; business process execution language for Web services(BPEL4WS); verification of Web services composition; analysis of workflow model



0 引言

Web服務(wù)組合是以復(fù)雜的需求為目標(biāo)，設(shè)計(jì)已有的相對(duì)簡(jiǎn)單的Web服務(wù)間的交互關(guān)系，從而形成一個(gè)滿足需求的新服務(wù)。這種新的架構(gòu)帶來了更高的重用性、可擴(kuò)展性，降低了耦合性，緩和了空間的敏感度。在服務(wù)組合的實(shí)施過程中，一個(gè)復(fù)雜的需求會(huì)涉及很多簡(jiǎn)單服務(wù)，流程的復(fù)雜性和并發(fā)性，使得人工進(jìn)行正確性與有效性驗(yàn)證變得異常困難。而Web服務(wù)交互協(xié)議的驗(yàn)證對(duì)于Web服務(wù)的實(shí)現(xiàn)、應(yīng)用與組合有重要意義，即通過驗(yàn)證可以證明一個(gè)Web服務(wù)的控制流滿足某個(gè)重要或者期望的屬性。

當(dāng)前，Web服務(wù)組合的研究成為人們關(guān)注的熱點(diǎn)問題，OWLS^[1]和BPEL4WS^[2]是當(dāng)前被廣泛使用的Web服務(wù)描述語言，它們被用于服務(wù)組合的建模和實(shí)現(xiàn)。但是，有關(guān)它們的驗(yàn)證方法卻很少被人們關(guān)注^[3]。文獻(xiàn)[4]提出了一種以Spin對(duì)OWLS流程進(jìn)行檢驗(yàn)的方法；文獻(xiàn)[5]用ConGolog對(duì)OWLS描述的服務(wù)進(jìn)行組合；文獻(xiàn)[6]使用Petri網(wǎng)作為Web服務(wù)組合的建模語言；文獻(xiàn)[7]曾提出用Petri 網(wǎng)來驗(yàn)證BPEL流程組合。然而，Petri網(wǎng)的可達(dá)集在網(wǎng)的規(guī)模上是以指數(shù)形式增長(zhǎng)的，雖然模型可能有界，但已超出當(dāng)前計(jì)算機(jī)的處理能力。為此，本文提出一種新的Web服務(wù)驗(yàn)證方法，使用TLA（temporal logic of action）^[8]對(duì)OWLS和BPEL4WS流程進(jìn)行建模。

TLA 表達(dá)能力強(qiáng)，且采用模塊化、層次化的描述方法使得條理清晰、脈絡(luò)分明。另外，TLA＋模型檢驗(yàn)器TLC 采用多個(gè)工作線程并發(fā)檢驗(yàn)的方法以加快驗(yàn)證速度，并利用磁盤技術(shù)來緩解狀態(tài)爆炸問題。所以，與其他驗(yàn)證工具相比，使用TLA 進(jìn)行描述并驗(yàn)證具有一定優(yōu)勢(shì)，不用像Spin 那樣擔(dān)心無法處理實(shí)時(shí)，像UPPAAL那樣擔(dān)心表達(dá)能力有限和內(nèi)存消耗過大。本文對(duì)OWLS的建模是服務(wù)為黑盒，而對(duì)BPEL4WS的描述則是白盒的，需要根據(jù)服務(wù)內(nèi)部的信息，將服務(wù)描述為自動(dòng)機(jī)。這兩種建模方式采用了不同的描述粒度，可以根據(jù)具體的驗(yàn)證需求進(jìn)行選擇。

1 OWLS和BPEL4WS流程模型

在OWLS流程（process）模型^[1]中，包含各種控制結(jié)構(gòu)，如順序結(jié)構(gòu)、并發(fā)產(chǎn)生結(jié)構(gòu)、并發(fā)同步結(jié)構(gòu)、條件結(jié)構(gòu)以及非確定性選擇結(jié)構(gòu)等。它們均以嵌套的XML格式表示，上層控制結(jié)構(gòu)在外，下層在內(nèi)，因此容易表示成如圖1所示的樹型結(jié)構(gòu)。在圖1中，每個(gè)內(nèi)部節(jié)點(diǎn)表示一種控制結(jié)構(gòu)，葉子節(jié)點(diǎn)表示原子服務(wù)。例如，根節(jié)點(diǎn)find cheaper book是sequence結(jié)構(gòu)，表示其三個(gè)兒子節(jié)點(diǎn)將順序執(zhí)行；find price節(jié)點(diǎn)是split結(jié)構(gòu)，其兩個(gè)兒子節(jié)點(diǎn)將并發(fā)執(zhí)行。

圖1的OWLS示例描述了這樣一個(gè)運(yùn)作過程。首先，根據(jù)客戶提供的圖書名，從Amazon和BN兩個(gè)網(wǎng)站獲取該圖書的價(jià)格，并比較之；然后將價(jià)格較低的網(wǎng)站提供的圖書信息反饋給客戶。這個(gè)示例足夠簡(jiǎn)單，且包括了順序、選擇以及富有代表性的并發(fā)流程。

Web服務(wù)的業(yè)務(wù)流程執(zhí)行語言(BPEL4WS)能夠?qū)崿F(xiàn) Web 服務(wù)調(diào)用、操縱數(shù)據(jù)、拋出故障或終止一個(gè)流程等不同功能，并且可以將它們連接起來，創(chuàng)建出復(fù)雜的流程。作為可執(zhí)行流程的實(shí)現(xiàn)語言，BPEL4WS 的作用是將一組現(xiàn)有的服務(wù)整合起來，從而定義一個(gè)新的 Web 服務(wù)。因此，BPEL4WS 基本上是一種實(shí)現(xiàn)這樣的整合語言。BPEL4WS 流程有著與OWLS類似的流程表示。

2 用TLA做模式檢驗(yàn)

Web服務(wù)組合流程模型的復(fù)雜性與并發(fā)性使手工方式難以起到驗(yàn)證的作用。模式檢驗(yàn)（model checking）技術(shù)的采用在一定程度上解決了這個(gè)問題。模式檢驗(yàn)是一種在驗(yàn)證分布式系統(tǒng)中應(yīng)用相當(dāng)成功的方法，它能夠窮盡系統(tǒng)所有可能的執(zhí)行狀態(tài)，以驗(yàn)證某種屬性是否被滿足。模式檢驗(yàn)可以形式化地證明系統(tǒng)的正確性。

為了構(gòu)造關(guān)于系統(tǒng)正確性的證明，三方面內(nèi)容需要確定。第一，證明什么命題。一般情況下，有兩種性質(zhì)最常被檢驗(yàn)，即安全性（safety）和活性（liveness）。安全性保證不希望發(fā)生的事情永遠(yuǎn)不發(fā)生，如死鎖狀態(tài)；活性則表示希望發(fā)生的事情最終會(huì)發(fā)生。第二，抽象什么內(nèi)容。將關(guān)聯(lián)性不大的部分去除有利于減少模型的復(fù)雜性，進(jìn)一步確保窮盡分析所有可能的執(zhí)行狀態(tài)，順利完成檢驗(yàn)。經(jīng)過簡(jiǎn)化的模型抓住了系統(tǒng)設(shè)計(jì)的精要部分，避免完整系統(tǒng)的繁復(fù)性，能夠較為簡(jiǎn)單地被驗(yàn)證；而與之相應(yīng)的完整系統(tǒng)甚至有無法驗(yàn)證的可能。第三，怎樣為協(xié)議建模。這是進(jìn)行驗(yàn)證的直接前提。而要生成交互協(xié)議的驗(yàn)證模型，就必須將交互協(xié)議轉(zhuǎn)換為形式化規(guī)約；然后將得到的規(guī)約輸入模式檢驗(yàn)工具，如TLC，才能自動(dòng)驗(yàn)證該協(xié)議是否滿足某個(gè)命題。

時(shí)序邏輯作為一種描述動(dòng)態(tài)系統(tǒng)行為和性質(zhì)的邏輯語言，近年來在實(shí)時(shí)系統(tǒng)的表示與驗(yàn)證、網(wǎng)絡(luò)協(xié)議的分析、人工智能等方面得到了廣泛應(yīng)用。本文采用的數(shù)時(shí)序邏輯語言稱為TLA。TLA^[8，9]是描述離散時(shí)序動(dòng)態(tài)系統(tǒng)的一種重要的時(shí)序邏輯，它結(jié)合了標(biāo)準(zhǔn)時(shí)序邏輯和活動(dòng)邏輯的特點(diǎn)。TLA的公式中包含一些經(jīng)典的數(shù)學(xué)符號(hào)：∧和∨；與；一元操作符□和◇等等。TLA的語義解釋基于行為（behavior）、狀態(tài)（state）和動(dòng)作（action）三個(gè)概念。行為是一個(gè)無限的狀態(tài)序列，用σ表示；狀態(tài)是TLA的變量到具體變量值的一個(gè)映射，所有可能狀態(tài)的集合用St表示；動(dòng)作代表了當(dāng)前狀態(tài)與下一狀態(tài)之間的關(guān)系。TLA的另一特點(diǎn)是，其規(guī)約可模塊化，即可以將子系統(tǒng)的規(guī)約作為一個(gè)模塊，在完整系統(tǒng)中進(jìn)行使用。例如：假設(shè)有一個(gè)時(shí)鐘，選取變量hr表示它的小時(shí)數(shù)(只考慮整數(shù))，于是，時(shí)鐘的運(yùn)行狀態(tài)如下：

[hr=1]→[hr=2]→…→ [hr=12]→[hr=1]→…



其中：每一個(gè)hr的取值均表示時(shí)鐘的一個(gè)狀態(tài)，諸如[hr=11]→[hr=12]的狀態(tài)變遷就是動(dòng)作，而由hr所表示的狀態(tài)序列就是一個(gè)行為。這個(gè)簡(jiǎn)單的時(shí)鐘模型用TLA描述，其表示的形式如下：

MODULE HourClock 

EXTENDS Naturals \\*引入Naturals模塊

VARIABLE hr \\*定義變量hr

HCini=hr \\in (1 .. 12) \\*初始化

HCnxt =hr′ = IF hr # 12 THEN hr + 1 ELSE 1 

\\*狀態(tài)變化規(guī)則(nextstation relation)

HC=HCini /\\ [][HCnxt]_hr \\*完整系統(tǒng)定義



THEOREMHC => []HCini \\*對(duì)于HC的任何

行為，HCini必須為真



其中：“\\*”表示注釋；帶“′”號(hào)的變量表示下一狀態(tài)時(shí)刻的該變量。一個(gè)TLA定義就是一個(gè)關(guān)于系統(tǒng)行為的規(guī)約，一般由初始化謂詞、狀態(tài)轉(zhuǎn)移規(guī)則、完整系統(tǒng)定義、定理（theorem）幾部分組成。在這個(gè)例子中，時(shí)鐘的初始狀態(tài)要滿足HCini，而它的每一步狀態(tài)變遷均必須符合狀態(tài)轉(zhuǎn)移規(guī)則[HCnxt]_hr，時(shí)序符號(hào)[]就用來表示[HCnxt]_hr總是為真。其中，[HCnxt]_hr稱為stutter step，表示[HCnxt]∨(hr′=hr)，即hr或者滿足HCnxt或者不變。為了用一個(gè)簡(jiǎn)約的表示系統(tǒng)規(guī)約，最后用HC將HCini和HCnxt寫入一個(gè)表達(dá)式。定理的意思是任何行為均滿足的時(shí)序公式，因?yàn)楦鶕?jù)系統(tǒng)規(guī)約HC，HCini總是為真的，因此HC  []HCini就是一個(gè)定理。

從這個(gè)例子不難發(fā)現(xiàn)，TLA通過變量的選取來描述系統(tǒng)的狀態(tài)，所以TLA具有靈活、描述能力強(qiáng)的特點(diǎn)。同時(shí)，如何選取變量來描述系統(tǒng)就成為使用TLA建模的關(guān)鍵。下一部分將詳述如何對(duì)OWLS和BPEL4WS中的流程進(jìn)行建模。

3 OWLS和BPEL4WS流程模型轉(zhuǎn)換為TLA

3. 1 用TLA為OWLS流程建模（圖2）

為了將OWLS的流程模型轉(zhuǎn)換成TLA描述，有一個(gè)問題需要確定，即抽取OWLS流程模型的哪方面信息進(jìn)行映射。概括而言，OWLS的流程模型有三個(gè)主要方面，即信息轉(zhuǎn)換、狀態(tài)遷移和控制流。信息轉(zhuǎn)換即服務(wù)的輸入和輸出；狀態(tài)遷移，即preconditions和effects，大意是現(xiàn)實(shí)世界的某種狀態(tài)，如購(gòu)物錢款已經(jīng)打入賣家的賬戶，或者商品已經(jīng)送達(dá)買家手中等等；而控制流則是描述了相互合作的各個(gè)服務(wù)之間的時(shí)序關(guān)系。這里，著重抽取OWLS流程模型的控制流信息，并轉(zhuǎn)換為TLA描述。

首先將OWLS流程模型轉(zhuǎn)換為常規(guī)的有向圖表示方法。這時(shí)，某個(gè)節(jié)點(diǎn)的前驅(qū)和后繼節(jié)點(diǎn)均能夠輕易求得，再引入TLA，為節(jié)點(diǎn)間的時(shí)序關(guān)系建模。

為了描述OWLS流程，以TLA中的behavior表示流程的一次執(zhí)行。顯然，behavior中的各個(gè)狀態(tài)的變化反映了流程的執(zhí)行過程。引入常量start、end表示流程開始和結(jié)束的活動(dòng)。此外，為了描述工作流的執(zhí)行過程，需要引入兩個(gè)變量。

定義1 引入P為一個(gè)集合變量。其中的元素代表流程執(zhí)行過程中已經(jīng)執(zhí)行完畢的子服務(wù)。

定義2 引入V為一個(gè)集合變量。其中的元素代表流程執(zhí)行過程中正在執(zhí)行的子服務(wù)。

對(duì)OWLS流程模型中的每一種控制結(jié)構(gòu)，本文均用一個(gè)TLA的action來表示。

定義3 Sequence（Si，Sj）==(Si ∈V) ∧ (P′=P ∪ {Si })∧(V′=V ∪ { Sj }-{ Si })。其中:Sj是Si的后繼服務(wù)。

定義4 Split（Si， Si1， Si2， …，Sin）==(Si ∈V) ∧ (P′ = P ∪ {Si}) ∧ (S′= S ∪ {Si1，Si2，…，Sin}–{Si})。其中：Si是分支點(diǎn)的前驅(qū)服務(wù)；Si1，Si2，…，Sin是分支點(diǎn)后分出的并行服務(wù)。

定義5 SplitJoin（Si，Si1，Si2，…，Sin）==({Si1， Si2，…，Sin}V) ∧ (P′ = P ∪{Si1， Si2，…，Sin}) ∧ (V′ = V ∪ {Si}-{Si1，Si2，…，Sin})。其中：Si1，Si2，…，Sin是匯合點(diǎn)的前驅(qū)并行服務(wù)；Si是匯合后的服務(wù)。

定義6 Choice(Si， Si1，Si2，…，Sin)==(branch1∧branch2∧branch3∧…∧branchn) ∨(branch1∧branch2∧branch3∧…∧branchn)∨…∨(branch1∧branch2∧branch3∧…∧branchn)。其中:branchk==(Si ∈V)∧(P′=P ∪ {Si})∧(S′=S ∪ {Sik}-{Si}); k=1，2，…，n；Si是分支點(diǎn)的前驅(qū)服務(wù)；Si1，Si2，…，Sin是分支點(diǎn)的后繼服務(wù)。

定義7 Repeat(Si)==(Si ∈ V)∧(P′=P)∧(V′=V)，其含義是服務(wù)Si反復(fù)執(zhí)行。

定義8 IfThenElse（Si，Sj，Sk）==(Si∈V)∧(P′=P∪{Si})∧(if condition then (V′=V∪{Sj}-{Si}) else(V′=V∪{Sk}-{Si}))。其中：Sj是condition為真時(shí)執(zhí)行的服務(wù)；Sk是為假時(shí)執(zhí)行的服務(wù)。在實(shí)際處理中，因?yàn)榉种l件往往與具體服務(wù)的輸出相關(guān)，難以進(jìn)行描述，故可以將該控制結(jié)構(gòu)簡(jiǎn)化為choice結(jié)構(gòu)。

3. 2 用TLA為BPEL4WS流程建模

3. 2. 1 Web服務(wù)的有限自動(dòng)機(jī)模型

一個(gè)組合服務(wù)可以表示為元組S=(P，Msg， A1，A2，…，An)。其中：P是單個(gè)原子服務(wù)的集合；Msg是全局消息類型的集合；A1，A2，…，An為各個(gè)原子服務(wù)的mealy自動(dòng)機(jī)，Ai=(Mini，Mouti，T，si，F(xiàn)i，Δi)。其中：Mini(Mouti)是某個(gè)服務(wù)的消息類型集合；T，si，F(xiàn)i分別是狀態(tài)集合、初始狀態(tài)和終態(tài)集合；Δi表示狀態(tài)遷移函數(shù)，它有三種行為：a)向原子服務(wù)發(fā)送消息m，將m添加到接收者隊(duì)列，狀態(tài)從q1變?yōu)閝2；b)接收一個(gè)消息，放到自己的消息隊(duì)列，然后消費(fèi)該消息，實(shí)現(xiàn)狀態(tài)從q1到q2的轉(zhuǎn)換；c)沒有消息可以收發(fā)。而從全局角度出發(fā)，給定的組合服務(wù)S=(P，Msg，A1，A2，…，An)，可以看做是一個(gè)整體的大服務(wù)，其mealy自動(dòng)機(jī)表示為(Min，Mout，T，s，F(xiàn)，Δ)。其中：Min和Mout表示全局消息隊(duì)列；T、s、F、Δ分別表示狀態(tài)集合、初始狀態(tài)和終態(tài)集合。

可以定義cs→cs′的狀態(tài)變遷，當(dāng)且僅當(dāng)某個(gè)組件服務(wù)發(fā)生遷移τ∈Δi。因此，組合服務(wù)CS的運(yùn)行可以看做是有限序列：cs0，cs1，…，cs|cs|，發(fā)送消息將分別加入接收服務(wù)和全局記錄w的消息序列中。

以上就是Web服務(wù)組合之狀態(tài)機(jī)模型的概述，本文主要研究如何使用TLA對(duì)這個(gè)模型實(shí)施驗(yàn)證。

3. 2. 2 BPEL4WS轉(zhuǎn)換為自動(dòng)機(jī)模型

如前所述，組合服務(wù)的自動(dòng)機(jī)模型的每個(gè)組件服務(wù)均是包含先進(jìn)先出消息隊(duì)列的mealy自動(dòng)機(jī)。于是，要將BPEL4WS轉(zhuǎn)換為自動(dòng)機(jī)，主要有兩個(gè)步驟：a)按一定的規(guī)則生成服務(wù)之間交互的消息;b)根據(jù)每個(gè)BPEL4WS的流程結(jié)構(gòu)生成相應(yīng)的mealy自動(dòng)機(jī)。

1)消息生成

BPEL4WS中有〈invoke〉 〈receive〉和〈reply〉等活動(dòng)，針對(duì)每個(gè)活動(dòng)以及其中包含的信息可以生成相應(yīng)消息，規(guī)則可以根據(jù)需求定義。本文中，假設(shè)組合服務(wù)以及所有原子服務(wù)的〈partner〉以及〈serviceLinkType〉保持一致，則消息生成的算法如下：

a)〈invoke〉活動(dòng)。如果該活動(dòng)的outputVariable屬性值為空（表示異步操作，調(diào)用后沒有返回值），生成消息sOwner_Operation_IN。這里sOwner是被調(diào)用的Web服務(wù)的名字，Operation是該活動(dòng)的operation屬性值。如果該活動(dòng)的outputVariable屬性值不為空（表示同步操作，有返回值），在生成消息sOwner_Operation_IN之外，再生成消息sOwner_Operation_OUT， sOwner與Operation含義同上。

b)〈receive〉活動(dòng)。生成記為Owner_Operation_IN消息。這里，Owner是〈receive〉活動(dòng)所在Web服務(wù)的名字，Operation是該活動(dòng)的operation屬性值。

c)〈reply〉活動(dòng)。生成Owner_Operation_OUT消息。這里，Owner是〈reply〉活動(dòng)所在Web服務(wù)的名字，Operation是該活動(dòng)的operation屬性值。

2)BPEL4WS文檔轉(zhuǎn)換為mealy自動(dòng)機(jī)

a)將基本活動(dòng)轉(zhuǎn)換為一個(gè)自動(dòng)機(jī)^[10]。

b)結(jié)構(gòu)化活動(dòng)中可能包含基本活動(dòng)和結(jié)構(gòu)化活動(dòng)。算法基本思想是按一定的規(guī)則，將其所包含活動(dòng)對(duì)應(yīng)的自動(dòng)機(jī)組合成一個(gè)大的自動(dòng)機(jī)。這里僅討論〈sequence〉和〈flow〉活動(dòng)，其他的結(jié)構(gòu)化活動(dòng)可以用類似的方式處理。

〈sequence〉:只要將包含的所有活動(dòng)首尾相連即可，如圖7所示。

〈flow〉:首先找出滿足link條件的一系列活動(dòng)（圖8），再將這些活動(dòng)對(duì)應(yīng)的自動(dòng)機(jī)作笛卡兒乘積。

假設(shè)有自動(dòng)機(jī)A1(Ain1，Mout1，T1，s1，f1，Δ1)和A2(Min2，Mout2，T2，s2，F(xiàn)2，Δ2) ，則A1×A2(A1和A2的笛卡爾積)得到一個(gè)新自動(dòng)機(jī)A(Min，Mout，T，s，F(xiàn)，Δ)，且有

a)Min=Min1∪Min2;

b)Mout=Mout1∪Mout2;

c)T=T1×T2;

d)s=（s1，s2）;

e)F是滿足以下條件的狀態(tài)：對(duì)于si∈T1，sj∈T2，(si，sj)∈F當(dāng)且僅當(dāng)sj∈F2；

f)如果Δ1或Δ2中存在τ=(x，info， y)（info是狀態(tài)轉(zhuǎn)移中所帶的信息，具體指!m，?m和ε），則對(duì)于任意τ所不屬于的那個(gè)自動(dòng)機(jī)的狀態(tài)si，如果(x，si)∈T1×T2且(y，si)∈T1×T2，則τ′=((x，si)，info，(y，si))∈Δ。

3. 2. 3 轉(zhuǎn)換為TLA

利用自動(dòng)機(jī)模型將服務(wù)組合系統(tǒng)描述為TLA表達(dá)式，其算法如下。

設(shè)基于自動(dòng)機(jī)模型的組合服務(wù)S=(P， Msg， A1，A2，A2，…，An)

a)對(duì)每個(gè)服務(wù)Si引入變量curstatei與Qi；這里，curstatei屬于Ti，表示服務(wù)的當(dāng)前狀態(tài)，Qi表示該服務(wù)的消息隊(duì)列。

b)初始化，Ai∈S有curstatei=si，Qi=〈〉，將它們合取，得到init表達(dá)式。

c)(a)對(duì)發(fā)送消息的每個(gè)Si，假設(shè)消息被Sk接收，則添加一個(gè)動(dòng)作:

Si_send =

∧curstate = q1

∧append(Qk，msg)

∧curstate′i = q2

∧UNCHANGED 〈other variables〉。



表達(dá)式中，curstatei 從q1遷移到q2，msg被存放在服務(wù)Sk的消息隊(duì)列中，其他變量保持不變。

(b)對(duì)每個(gè)接收消息的服務(wù)Si，添加動(dòng)作:

Si_receive =

∧curstatei = q1

∧head(Qi) = msg

∧tail(Qi)

∧curstate′i = q2

∧UNCHANGED 〈other variables〉。



curstatei從q1遷移到q2。若msg在Si消息隊(duì)列的頭部，則刪除它，其他值保持不變。

d)針對(duì)組合服務(wù)一次執(zhí)行終止時(shí)的狀態(tài)，添加動(dòng)作：

S_step_reset =

∧Si∈S:cursatei∈Fi，Qi=〈〉

∧Si∈S:cursatei′=Si，Qi=〈〉。



該表達(dá)式表示當(dāng)所有服務(wù)均進(jìn)入自己的終態(tài)，且各自隊(duì)列為空時(shí)，所有變量恢復(fù)到初始狀態(tài)，開始新一輪的運(yùn)行周期。

e)將步驟c)和d)中得到的表達(dá)式析取，得到next表達(dá)式。

f)得出整個(gè)系統(tǒng)的TLA表達(dá)式，spec=init∧[][next]v（v是所有變量組成的元組）。

4 轉(zhuǎn)換工具的設(shè)計(jì)與實(shí)現(xiàn)

4. 1 OWLS2TLA

OWLS以XML為基礎(chǔ)，對(duì)流程模型進(jìn)行描述。各種控制結(jié)構(gòu)以相應(yīng)的標(biāo)簽明示，其子結(jié)構(gòu)嵌套其中。因此，OWLS流程模型的描述可以很方便地映射為樹型結(jié)構(gòu)，外層標(biāo)簽是相鄰內(nèi)層標(biāo)簽的父親節(jié)點(diǎn)，正如圖1所示。為了將流程模型的樹型結(jié)構(gòu)描述轉(zhuǎn)換為TLA描述，引入圖9所示的流程模型。

根據(jù)3.1節(jié)提出的流程控制結(jié)構(gòu)描述方式，只要找出圖9中某個(gè)節(jié)點(diǎn)的所有前驅(qū)節(jié)點(diǎn)以及控制結(jié)構(gòu)類型，就不難得到OWLS流程模型的TLA描述。整個(gè)工具的處理方式如圖10所示。

最后，將生成的TLA文檔輸入TLC，即可進(jìn)行驗(yàn)證工作。

4. 2 BPEL2TLA

根據(jù)前面的討論本文開發(fā)了一個(gè)BPEL4WS轉(zhuǎn)換為TLA文檔的工具。

該轉(zhuǎn)換工具讀入組合服務(wù)的BPEL4WS文檔，生成組合服務(wù)的自動(dòng)機(jī)模型，接著再轉(zhuǎn)換為TLA表達(dá)式并生成TLA文檔。得到TLA描述文檔后，使用TLC檢驗(yàn)工具就可以對(duì)系統(tǒng)進(jìn)行驗(yàn)證。

具體實(shí)現(xiàn)該工具時(shí)，是在開源的Web服務(wù)驗(yàn)證工具WSAT的基礎(chǔ)上進(jìn)行開發(fā)的，沿用了該工具的很多數(shù)據(jù)結(jié)構(gòu)以及類的設(shè)計(jì)，修改了相應(yīng)的代碼以滿足自動(dòng)機(jī)模型，并添加了自動(dòng)機(jī)轉(zhuǎn)換為TLA的模塊。系統(tǒng)模塊如圖11所示。

5 實(shí)驗(yàn)與分析

給定一個(gè)OWLS流程模型的TLA描述，作為TLC的輸入。TLC可以模擬流程模型的執(zhí)行，檢查指定的命題是否被滿足?？蓹z驗(yàn)的屬性包括某個(gè)變量在某個(gè)時(shí)刻的值、執(zhí)行狀態(tài)以及執(zhí)行路徑等。在這部分內(nèi)容中，筆者將舉例說明幾種可以實(shí)施的驗(yàn)證。

對(duì)于圖1中的示例，按照之前所述的各種控制結(jié)構(gòu)的TLA描述方式，不難得到該流程的完整TLA定義。首先，使用TLC工具對(duì)得到的TLA文件進(jìn)行默認(rèn)驗(yàn)證，檢驗(yàn)死鎖屬性，結(jié)果如下：

12 states generated， 10 distinct states found， 0 states left on queue. The depth of the complete state graph search is 7



從TLC的輸出結(jié)果可以看到，整個(gè)流程共產(chǎn)生12個(gè)狀態(tài)。其中相互不同的狀態(tài)有10個(gè)，狀態(tài)圖搜索的深度為7，沒有死鎖出現(xiàn)。

若對(duì)流程進(jìn)行修改，使FindBNPrice服務(wù)阻塞。TLC檢驗(yàn)結(jié)果如下：

Error deadlock reached. The behavior up to this point is:

STATE 1: 〈Initial predicate〉

∧P = {}， ∧V= {\"Start\"}

STATE 2: 〈Action line 7…〉

∧p = {\"Start\"}， ∧V= {\"FindBookInfo\"}

STATE 3: 〈Action line 9…〉

∧p = {\"Start\"， \"FindBookInfo\"}， 

∧V= {\"FindAmazonPrice\"}



根據(jù)這些信息就能找出導(dǎo)致死鎖的原因，以作適當(dāng)修改。

如圖12所示，客戶端調(diào)用雇員出差安排業(yè)務(wù)流程，指定雇員的相關(guān)信息(如姓名、目的地、出發(fā)日期及返回日期等)。此BPEL4WS流程先調(diào)用雇員出差狀態(tài)Web服務(wù)檢查雇員出差狀態(tài)；然后BPEL4WS流程將檢查以下Alpha航空公司和Beta航空公司兩家航空公司的機(jī)票價(jià)格，選擇較低的價(jià)格并將出差計(jì)劃返回給客戶端。

使用上述轉(zhuǎn)換工具將組合系統(tǒng)轉(zhuǎn)換為TLA文檔，除了需要組合服務(wù)的BPEL4WS和WSDL描述文檔之外，還要提供所涉及的所有原子服務(wù)的BPEL4WS描述文檔。將組合服務(wù)以及所有原子服務(wù)的BPEL4WS和WSDL文檔輸入該轉(zhuǎn)換工具，可得運(yùn)行結(jié)果。

首先，將每個(gè)BPEL文檔轉(zhuǎn)換為自動(dòng)機(jī)，包括每一個(gè)自動(dòng)機(jī)的狀態(tài)集、初始狀態(tài)、最終狀態(tài)集合以及所有的轉(zhuǎn)移函數(shù)，在每個(gè)轉(zhuǎn)移函數(shù)后面給出了該函數(shù)對(duì)應(yīng)的基本活動(dòng)，以及與該活動(dòng)交互的Web服務(wù)的名稱。需要說明的是，這里輸出的自動(dòng)機(jī)經(jīng)過了處理，由原來的NFA轉(zhuǎn)換為DFA，并除去了冗余狀態(tài)和轉(zhuǎn)移函數(shù)。接著，利用3.2.3節(jié)中的算法將合成服務(wù)轉(zhuǎn)換為一個(gè)TLA文檔。輸入至TLC，驗(yàn)證結(jié)果如下：

48 states generated， 32 distinct states found， 0 states left on queue. The depth of the complete state graph search is 17



這里，TLC根據(jù)TLA描述文檔生成了32種不同狀態(tài)，檢測(cè)這些狀態(tài)，并得出系統(tǒng)不存在死鎖的結(jié)論。

為構(gòu)造死鎖（deadlock）的實(shí)例，現(xiàn)在將雇員出差安排的BPEL4WS流程修改，假設(shè)流程調(diào)用（invoke）Alpha航空公司W(wǎng)eb服務(wù)后沒有等待接收回調(diào)（callback）而直接進(jìn)入后面過程，將修改過的BPEL4WS文檔生成的TLA文檔輸入TLC， 驗(yàn)證結(jié)果如下：

Error deadlock reached. The behavior up to this point is:

STATE 1: 〈Initial predicate〉

∧ pQueue = [ BusinessTravelProcess |-〉 〈〉，

Employee |→ 〈〉，

DeltaAirline |→ 〈〉，

AmericanAirline |→ 〈〉，

Client |→ 〈 }

……

60 states generated， 38 distinct states found， 0 states left on queue. The depth of the complete state graph search is 16



TLC檢測(cè)到系統(tǒng)存在死鎖并給出了產(chǎn)生死鎖的路徑，根據(jù)這些信息可以找到死鎖的原因，并作出相應(yīng)的修改。

6 結(jié)束語

隨著因特網(wǎng)的發(fā)展，越來越多的企業(yè)和組織開始提供并發(fā)布Web服務(wù)，建立虛擬社區(qū)以實(shí)現(xiàn)大規(guī)模信息共享。而Web服務(wù)也愈來愈稱為解決復(fù)雜環(huán)境中信息交互與整合問題的主要技術(shù)。然而Web服務(wù)的應(yīng)用面對(duì)著許多問題，例如，如何組合服務(wù)、自動(dòng)服務(wù)組合的可行性、服務(wù)組合的驗(yàn)證等。本文利用了一種新技術(shù)TLA作為驗(yàn)證組合正確性的手段，涉及的問題包括：如何用TLA為流程建模，如何將工業(yè)界的流程描述語言轉(zhuǎn)換為TLA、自動(dòng)轉(zhuǎn)換工具的實(shí)現(xiàn)，以及利用TLC驗(yàn)證Web服務(wù)組合。

本文只是使用TLA驗(yàn)證Web服務(wù)組合的第一步，主要討論了安全性驗(yàn)證。筆者下一步的工作會(huì)更多研究活性與安全性驗(yàn)證，以及用模式檢驗(yàn)方法建立粒度更小、描述更為精確的Web服務(wù)組合模型并加以驗(yàn)證。

參考文獻(xiàn)：

[1]W3C Member. OWLS: semantic markup for Web services [EB/OL]. [20041122]. http://www.w3.org/Submission/OWLS/ .

[2]Business process executive language for Web service version 1.0[EB/OL]. (20020730). http://www106.ibm.com/developerworks/library/wsbpel. 

[3]HUANG Hai， MASON R A. Model checking technologies for Web services[C]//Proc of the 4th IEEE Workshop on Software Technologies for Future Embedded and Ubiquitous Systems， and the 2nd International Workshop on Collaborative Computing， Integration， and Assurance. Washington DC: IEEE Computer Society， 2006:217224.

[4]ANKOLEKAR A， PAOLUCCI M， SYCARA K. Spinning the OWLS process model: toward the verification of the OWLS process models[C]//Proc of the 3rd Semantic Web Services: Preparing to Meet the World of Business Applications， a Workshop at 3rd International Semantic Web Conference (ISWC 2004). 2004.

[5]PHAN M， HATTORI F. Automatic Web service composition using conGolog[C]//Proc of the 26th IEEE International Conference. Washington: IEEE Computer Society， 2006:17.

[6]HAMADI R， BENATALL B. A Petri netbased model for Web service composition[C]//Proc of the 14th Australasian Database Conference. Darlinghurst: Australian Computer Society， 2003:191200.

[7]NARAYANAN S， MCLLRAITH S A. Simulation， verification and automated composition of Web services[C]//Proc of the 11th International Conference on World Wide Web. New York: ACM Press， 2002:7788.

[8]LAMPORT L. TLAthe temporal logic of actions[EB/OL]. (20040202). http://research.microsoft.com/users/lamport/tla/tla.html.

[9]LAMPORT L. Introduction to TLA， SRC technical note 1994001[R]. Palo Alto: Digital Systems Research Center， 1994.

[10]FU X， BULTAN T， SU J. Analysis of interacting BPEL Web services[C]//Proc of the 13th International Conference World Wide Web (WWW). New York: ACM Press， 2004.