Web服務(wù)流程相容性和等價性分析

1、Web服務(wù)流程相容性和相似性分析1李喜彤范玉順(清華大學(xué)自動化系北京100084)摘 要 服務(wù)組合和服務(wù)替換是面向服務(wù)計算的研究熱點，服務(wù)流程的相容性和相似性分 析是其中的兩個密切相關(guān)的問題，具有較大實用價值?；谥玃etri網(wǎng)建模 Web服務(wù)流程，定義服務(wù)流程的正確性和相容性。提出服務(wù)良構(gòu)性的概念，證明良構(gòu)性能夠保證組合服務(wù) 可達終止?fàn)顟B(tài)的正確性。在相容性分析的基礎(chǔ)上，提出服務(wù)流程相似性的定義，證明若新 服務(wù)與要被替換的服務(wù)流程相似，則所進行的替換是上下文無關(guān)的，替換后無須再做組合 正確性驗證，給出相似性的判定算法。結(jié)論和算法改進了現(xiàn)有服務(wù)組合驗證和服務(wù)替換方 法的不足。關(guān)鍵詞 Web服務(wù)

2、；服務(wù)組合；服務(wù)替換；相容性；相似性 中圖法分類號 TP311Analyzing Compatibility and Similarity of Web ServiceProcessesLI Xi-To ngFAN Y u-Shu n(Department of Automation, Tsinghua University, Beijing 100084 )Abstract Service composition and substitution are key research issues in Service-Oriented Computi ng (SOC). Among them,

3、 an alyz ing compatibility and similarity of Web service processes are two closely-related issues and of great importa nee. This paper models Web service processes using Colored Petri nets (CPN) and presents the definitions of correctness and compatibility of Web service processes. Then, the no ti o

4、n of well-structured ness of Web services is developed. The paper proves that all reachable final markings of a composite service composed by well-structured services are correct. Based on the compatibility analysis, the paper develops the definition of similarity of Web service processes in order t

5、o in vestigate service substituti on .It is con cluded that substitut ing a service in a compositi on can be performed in depe ndent of the con text as long as the new service is similar to the substituted one. There is thus no n eed to verify the substituted service compositi on aga in. The paper d

6、evelops an algorithm for verify ing similarity betwee n two services. The results and algorithm are used to improve the existing methods of service composition收稿日期：修改稿收到日期：本課題得到國家自然科學(xué)基金(60674080, 60704027)、國家“八六三”高技術(shù)研究發(fā)展計劃項目基金(2007AA04Z150)資助。李喜彤，男,1982年生，博士研究生，研究方向為 Web服務(wù)、面向服務(wù)計算、Petri網(wǎng)原理及應(yīng)用。E-mail:

7、lxt04。聯(lián)系地址：北京清華大學(xué)紫荊公寓14# 1218B (郵編:100084) 范玉順,男,1962年生,博士，教授，博士生導(dǎo)師，研究領(lǐng)域包括企業(yè)建模、工作流管理、面向服務(wù)體系架構(gòu)。verificati on and service substituti on.Key words Web service; service compositi on; service substituti on; compatibility; similarity1引言Web服務(wù)是目前面向服務(wù)體系架構(gòu)最流行的一種實現(xiàn)形式。單個Web服務(wù)通常無法滿足用戶需求，而需要將若干個 Web服務(wù)組合起來協(xié)同工作。服務(wù)組

8、合是指將若干個已存在的Web服務(wù)按照一定規(guī)則動態(tài)發(fā)現(xiàn)，并組裝成一個增值的、更粗粒度的服務(wù)或系統(tǒng)以滿足用戶的復(fù)雜需求。服務(wù)組合 已成為構(gòu)建面向服務(wù)、松散耦合、高適應(yīng)性的應(yīng)用系統(tǒng)的主要途徑1,2。組合服務(wù)的流程能否正確執(zhí)行直接影響到用戶需求是否能夠得到滿足，因此需要分析和驗證組 合服務(wù)流程的正確性，這方面的研究是當(dāng)前面向服務(wù)計算領(lǐng)域的一個熱點。服務(wù)組合的正確性可以 通過分析參與組合的各成員服務(wù)流程的相容性來進行驗證3,4。另一方面，服務(wù)替換是與服務(wù)組合密切相關(guān)的一個問題5。如果某個成員服務(wù)由于自身的軟硬件故障或者外部環(huán)境改變（如網(wǎng)絡(luò)阻塞、 病毒威脅）等原因不能繼續(xù)提供服務(wù)，那么將導(dǎo)致整個組合服務(wù)無

9、法正確執(zhí)行，用戶需求也就無法 得到滿足。此時需要發(fā)現(xiàn)并選取一個與失效服務(wù)的流程相似的服務(wù)來替換，以確保替換后的組合服 務(wù)仍然能夠正確執(zhí)行，也即需要保證替換服務(wù)與服務(wù)組合系統(tǒng)中的其他成員服務(wù)的流程相容。由此 可見，服務(wù)流程的相容性和相似性分析是兩個密切相關(guān)的問題，對于研究服務(wù)組合和服務(wù)替換具有 較大的應(yīng)用價值。由于驗證服務(wù)流程之間的相容性通常需要對整個組合服務(wù)的流程進行分析。在服務(wù)替換頻繁發(fā)生的情況下，不斷重復(fù)的服務(wù)組合驗證將耗費大量時間和資源，嚴(yán)重影響系統(tǒng)運行效率5。因此服務(wù)相似性定義需要與上下文無關(guān)，即在不需要驗證組合服務(wù)全局流程的情況下就能判斷選取的替換 服務(wù)如果與被替換服務(wù)相似，那么就能

10、夠與服務(wù)組合系統(tǒng)中的其他成員服務(wù)相容，從而保證替換后 的組合服務(wù)的流程仍然是正確的。分析Web服務(wù)的流程通常需要借助某種形式化方法，主要有基于有限狀態(tài)機的方法3、基于進程代數(shù)（或PI-演算）的方法和基于Petri網(wǎng)的方法2,6,7等。由于Petri網(wǎng)適合于對 Web服務(wù)這種松 散耦合的分布式系統(tǒng)進行建模，因此本文采用Petri網(wǎng)作為服務(wù)流程分析的理論基礎(chǔ)。文獻2提出了基于著色Petri網(wǎng)的Web服務(wù)模型，給出了四種主要的組合運算。文獻6以著色Petri網(wǎng)為基礎(chǔ)提出了面向消息的Web服務(wù)模型，該模型側(cè)重于對Web服務(wù)元消息的描述及其對服務(wù)協(xié)同通信的影響。文獻8借助工作流理論對 Web服務(wù)流程進行

11、建模，研究了基于信任關(guān)系的Web服務(wù)工作流服務(wù)質(zhì) 量調(diào)度方法。雖然 Petri網(wǎng)能夠?qū)M合服務(wù)進行分析和驗證，但是上述研究成果都沒有對此進行深入討論，沒有指出具有哪些性質(zhì)的兩個或多個服務(wù)的流程是相容的。進一步地，這些研究工作也都沒有涉及到服務(wù)流程的相似性和等價性分析。本文將組合服務(wù)看作是全局模型，而把各個參與組合的成員服務(wù)看作是局部模型?，F(xiàn)有研究工作大多是對組合服務(wù)的全局模型直接進行建模，較少考慮單個服務(wù)流程的正確性，因此無法揭示組合服務(wù)流程與單個服務(wù)流程之間的內(nèi)在關(guān)系。本文從組合服務(wù)的局部模型出發(fā)，基于著色Petri網(wǎng)建立單個服務(wù)流程模型，給出服務(wù)流程正確性的形式化定義。該定義不僅適用于單個

12、Web服務(wù)，同時也適用于刻畫組合服務(wù)的流程正確性。本文提出Web服務(wù)良構(gòu)性的概念，并指出成員服務(wù)的良構(gòu)性能夠保證組合服務(wù)可達終止?fàn)顟B(tài)是正確的，從而簡化了服務(wù)流程相容性分析的驗證條件。為了研究 具有哪些性質(zhì)的兩個服務(wù)可以進行替換，本文提出服務(wù)流程相似性和等價性的定義，并證明兩個流 程相似的良構(gòu)的服務(wù)可以進行與上下文無關(guān)的替換，替換后的組合服務(wù)的流程仍然是正確的。本文 討論了相似性與相容性之間的關(guān)系，并給出服務(wù)流程相似性判定算法。本文第2節(jié)給出有關(guān)的基本定義；第 3節(jié)分別討論服務(wù)流程的相容性和相似性；第4節(jié)介紹相關(guān)工作并進行對比討論；第5節(jié)給出結(jié)論和未來的工作。2 基本定義Petri網(wǎng)具有直觀的圖

13、形符號表示和堅實的理論分析技術(shù)，適合對 Web服務(wù)這種異步并發(fā)系統(tǒng)進行建模。然而基本Petri網(wǎng)在實際建模過程中存在一些固有不足9，因此本文采用著色Petri網(wǎng)建模Web服務(wù)的流程。有關(guān)著色Petri網(wǎng)的詳細內(nèi)容可參見文獻9。定義1( Web服務(wù)).Web服務(wù)是一個帶標(biāo)記的著色Petri網(wǎng)S = (N, A, L)，其中N為一著色Petri網(wǎng)，且滿足：(1) P是有限庫所集，ppIM pEM，其中：pic是服務(wù)流程內(nèi)部控制邏輯庫所集，PIM是內(nèi)部通信庫所集，PEM是服務(wù)與外界通信庫所集，PIC、PIM和PEM兩兩互不相交；(2) P中有兩個特殊的庫所，即：起始庫所i和終止庫所o，滿足L if，

14、 =-；(3) 如果去除庫所集 PEM以及所有與PEM關(guān)聯(lián)的弧，由此得到的Petri網(wǎng)稱為服務(wù)S對應(yīng)的工作 流網(wǎng)N，記為N二(S)。若在N上添加一個連接庫所 o到庫所i的變遷t* (即：LJt* = o , t*L = i)， 則N是強連通的；(4) -p P， p = i，滿足 Mj(i)=.一 且 Mj(p) =,其中 Mi是初始標(biāo)識；(5) A是標(biāo)記的非空有限集，a，A為一字符串型的標(biāo)識，其中A為一空標(biāo)記；(6) L是標(biāo)記函數(shù)，滿足 L : T > A。在定義1中，PEM中的每個庫所都對應(yīng)一個與外界通信的消息緩存區(qū)，每個與PEM連接的變遷稱為通信變遷，對應(yīng)一個與外界環(huán)境通信的操作(

15、如發(fā)送或接收消息)；服務(wù)流程內(nèi)部庫所包括 PIC和PIM兩部分，其中PIC表示內(nèi)部控制邏輯的狀態(tài)，而PIM表示內(nèi)部的消息緩存區(qū)；標(biāo)記集 A表示該服務(wù)所有可能的操作語義，A中的每一非空標(biāo)記字符串對應(yīng)該服務(wù)的一個操作命名；標(biāo)記函數(shù)L將服務(wù)模型中的每一個變遷映射到一個服務(wù)操作命名。而映射到空標(biāo)記.上的變遷所代表的操作行為是服務(wù)的內(nèi)部行為，即不被外界觀察到的行為。目前工業(yè)界已存在一些支持Web服務(wù)的業(yè)務(wù)流程建模語言，其中應(yīng)用最多的是業(yè)務(wù)流程執(zhí)行語言(Busin ess Process Executio n Lan guage, BPEL)，該語言已被 OASIS組織宣布為描述 Web服務(wù)流程 的標(biāo)準(zhǔn)。

16、需要指出的是，基于BPEL標(biāo)準(zhǔn)描述的 Web服務(wù)流程可以方便地轉(zhuǎn)換為本文定義1中的形式化模型。文獻10和11提出了基于BPEL的服務(wù)流程向Petri網(wǎng)服務(wù)模型轉(zhuǎn)換的具體方法，在此不再復(fù)述。本文主要研究如何利用定義1中的服務(wù)模型來形式化的分析Web服務(wù)流程的相容性和相似性。一個變遷t在標(biāo)識M下使能，記作：Mt 。若服務(wù)在標(biāo)識 M下通過實施變遷t后到達標(biāo)識M ，記作：Mt M I若服務(wù)在標(biāo)識 M下經(jīng)過實施一個變遷序列二-T*到達標(biāo)識M ，記作： M 二 M I所有從標(biāo)識M可達的標(biāo)識集記為：R(M)二M T*,M二M 。若標(biāo)識Mf滿足M f R(Mi) M f(o) = -，則稱M f為終止標(biāo)識，所

17、有終止標(biāo)識的集合記為M F。定義2 (正確的終止標(biāo)識). 服務(wù)S的終止標(biāo)識 Mf若滿足pPIC, p = o: M f (p)， 則稱M f為正確的終止標(biāo)識，記為Mcf。所有可達的正確終止標(biāo)識的集合記為Mcf。由定義2可知，正確的終止標(biāo)識要求終止庫所O中存在托肯，且其他的內(nèi)部控制邏輯庫所內(nèi)不能含有托肯。反之，如果終止庫所O與某個內(nèi)部控制邏輯庫所同時含有托肯，則表明該服務(wù)流程并沒有正確結(jié)束。定義 2中的正確終止?fàn)顟B(tài)并不要求所有非終止庫所都不能含有托肯，而可以在外部 或內(nèi)部通信庫所中留有未被消耗的托肯。這樣的要求符合Web服務(wù)基于消息通信且彼此松散耦合的本質(zhì)特性。定義3 (可達變遷序列).若變遷序

18、列廠-： t|,t2,.,tn，三T*滿足TM : Mj 二M，則稱為服務(wù)S的一個可達變遷序列。所有可達變遷序列的集合記為3(S)。定義4 (流程正確性). 服務(wù)S的流程是正確的，當(dāng)且僅當(dāng)在外界環(huán)境總是能夠滿足服務(wù)S對外部消息的需求的情況下，下列兩個條件同時滿足：(1) -M R(Mi)，如果 M ' Mf，則九三:(S)，使得 M二Mf MF ；(2) M CF = M F。定義4要求外界環(huán)境總是能夠滿足服務(wù)S對外部消息的需求， 也即：當(dāng)服務(wù)需要接收(或發(fā)送)消息時，外界環(huán)境總是能夠適時的發(fā)送(或接收)該消息。在這種情況下，排除了因外界環(huán)境導(dǎo)致 服務(wù)流程出現(xiàn)死鎖的情況。這樣的前提是合

19、理且可行的13。在實際分析過程中，只需要將服務(wù)的外部通信庫所 PEM以及所有與 PEM關(guān)聯(lián)的弧去除即可，即只需要考察服務(wù)S對應(yīng)的工作流網(wǎng)N -(S)。根據(jù)定義4,服務(wù)流程正確需要滿足兩個條件。第一個條件要求服務(wù)流程總是能夠到達終止標(biāo)識，不會發(fā)生死鎖；第二個條件則要求服務(wù)流程到達的終止標(biāo)識都必須是正確的終止標(biāo)識。3相容性和相似性分析3.1 相容性分析如果參與組合的若干成員服務(wù)中某個成員服務(wù)的流程不正確，那么該服務(wù)必將導(dǎo)致整個組合服 務(wù)的流程無法正確執(zhí)行。因此，本文在后續(xù)討論中均默認所有參與組合的成員服務(wù)的流程是正確的。 此時組合服務(wù)的流程能否正確執(zhí)行取決于各成員服務(wù)的流程是否相容。本組已有工作提

20、出了Web服務(wù)組合的形式化定義11,12，本文在此基礎(chǔ)上給出 Web服務(wù)流程相容性的定義。定義5 (服務(wù)流程相容). 設(shè)兩個服務(wù)S和能夠組合，其組合服務(wù) S = S,§ 。服務(wù)0和的流程是相容的，記為：sL s2，當(dāng)且僅當(dāng)組合服務(wù) s的流程是正確的。不難看出上述服務(wù)流程的相容性定義滿足對稱性，即：3L 二 EL 3。為了簡化相容性的驗證條件，本文考察一類具有良好結(jié)構(gòu)的Web服務(wù)，即“良構(gòu)”的Web服務(wù)。工作流理論通常要求所研究的工作流網(wǎng)是良構(gòu)的，即要求網(wǎng)結(jié)構(gòu)中由 And-Split發(fā)出的兩個并行分支必須由And-Join匯合，由Or-Split發(fā)出的兩個選擇分支必須由Or-Join匯

21、合。在工作流網(wǎng)“良構(gòu)性”orderoSnd moneyEM取i; jj.ni.'MR2Sfkl irJcr圖1 一個良構(gòu)的服務(wù)3morwyUser info圖2 一個非良構(gòu)的服務(wù) S2定義的基礎(chǔ)上14，本文提出Web服務(wù)良構(gòu)性的定義。定義6 (服務(wù)良構(gòu)性). 服務(wù)S是良構(gòu)的，當(dāng)且僅當(dāng)S對應(yīng)的工作流網(wǎng)N = ：(S)是良構(gòu)的。根據(jù)上述定義，易知圖1所示的服務(wù)S,是良構(gòu)的，而圖2所示的服務(wù)S2則是非良構(gòu)的。下面給出一個關(guān)于良構(gòu)的Web服務(wù)及其組合的重要結(jié)論。定理1.設(shè)兩個服務(wù)S,和S能夠組合，其組合服務(wù)。如果服務(wù)S、S2是良構(gòu)的，那么服務(wù)S從初始標(biāo)識可達的任一終止標(biāo)識都是正確的，即：Mcf

22、二Mf。證明(反證法)由于Mcf Mf，若Mcf=Mf,則 MMf，但Mf-MC 。由MMf ic可知，M f R(S,Mi)且M f(o) I一。由于M f M cf，根據(jù)定義2可知， p P ， p = o且Mf(p)式0。根據(jù)服務(wù)組合的定義可知11，PIC =RICupICui,o，若p = i，則Mf上Mf，使得M；(iJ式0且M ；(i2)0。因此不妨假設(shè) p乏PIC。由M f e Mf可知，服務(wù)S存在某個可 達的終止標(biāo)識 M使得Mg)工0且Mif(p)羊0。因為服務(wù)S,對應(yīng)的工作流網(wǎng) 口=(S)是 強連通的，那么網(wǎng) N,中存在一條從i,到o,的基本路徑 G使得p - G，并且存在一

23、條從i,到o,的基 本路徑C2使得p C2， C2 =G。進而可知，存在變遷t G * C2，而庫所q G * C2。這就與 服務(wù)S是良構(gòu)的前提產(chǎn)生矛盾。因此原命題得證。證畢根據(jù)定義4和定義5,判定兩個服務(wù)的流程是否相容需要驗證兩個條件，即：組合服務(wù)的流程總是能夠到達終止標(biāo)識，并且所有可達的終止標(biāo)識都是正確的。而定理1的結(jié)論實際上指出，由良構(gòu)的服務(wù)組合構(gòu)成的服務(wù)，如果從初始標(biāo)識能夠到達某個終止標(biāo)識，那么該終止標(biāo)識一定是正確的。由此可見，成員服務(wù)的良構(gòu)性有效的保證了組合服務(wù)可達終止標(biāo)識的正確性。因此，不難得到下面的結(jié)論。定理2.設(shè)兩個良構(gòu)的服務(wù) S)和s能夠組合，其組合服務(wù) s = s,二$。服

24、務(wù)S,和S,的流程是相容的，即：s,Ls2，當(dāng)且僅當(dāng)在外界環(huán)境總是能夠滿足服務(wù)s對外部消息的需求的情況下，-M R(Mi)，如果 M Mf，則二5 三:(S)，使得 ML M f MF。證明由定義4和定理1可直接得證。證畢.利用定理2的結(jié)論，在判定兩個良構(gòu)的服務(wù)是否流程相容時，只需要驗證其組合服務(wù)從初始標(biāo)識是否總是能夠到達終止標(biāo)識，而不會在某個標(biāo)識下發(fā)生死鎖的現(xiàn)象。需要指出的是，定理1和定理2的結(jié)論可以直接推廣到三個或三個以上服務(wù)組合的情況。據(jù)我們觀察，現(xiàn)實中獨立開發(fā)的大多數(shù)服務(wù)(如基于 BPEL的服務(wù)流程)都能夠遵循良構(gòu)性，因此利用定理2的結(jié)論可以大大簡化服務(wù)流程相容性的分析過程。3.2 相

25、似性分析分析服務(wù)流程的相似性對于研究服務(wù)發(fā)現(xiàn)和服務(wù)替換技術(shù)具有重要意義15。當(dāng)參與組合的某個成員服務(wù)由于某些原因不能繼續(xù)提供服務(wù)時，將導(dǎo)致組合服務(wù)無法正確執(zhí)行。此時需要發(fā)現(xiàn)并選取一個與失效服務(wù)的流程相似的服務(wù)來替換。在服務(wù)組合研究中，替換服務(wù)與被替換服務(wù)的流程相似 就必須要保證替換之后的組合服務(wù)仍然是正確的，也即需要保證替換服務(wù)的流程與服務(wù)組合系統(tǒng)中 其他成員服務(wù)的流程相容?？梢?，服務(wù)流程的相似性分析與相容性分析密切相關(guān)。由于相容性分析通常需要驗證組合服務(wù)全局流程的正確性。若替換頻繁發(fā)生，不斷重復(fù)的服務(wù) 組合驗證將耗費大量系統(tǒng)時間和資源5。因此，服務(wù)相似性定義需要與上下文無關(guān)，即在不需要驗證組

26、合服務(wù)全局流程的情況下就能判斷選取的替換服務(wù)如果與被替換服務(wù)相似，那么就能夠與服務(wù) 組合系統(tǒng)中的其他成員服務(wù)相容，從而保證替換后的組合服務(wù)的流程仍然是正確的。兩個服務(wù)相似并不一定要求兩者的內(nèi)部流程完全一致，而只需要兩者在與外界環(huán)境交互通信的 過程中表現(xiàn)出一定的相似性。因此，服務(wù)相似性的定義和分析主要關(guān)注服務(wù)表現(xiàn)出來的外部行為特 性。下面給出幾個關(guān)于服務(wù)外部行為特性的定義。定義7 (通信變遷序列).對于某個可達變遷序列匚Z (S)，若忽略匚中可能存在的內(nèi)部變遷，則得到相應(yīng)的通信變遷序列；=： t；,t2,.,tk ,其中L(t),丨=1,k。記得到相應(yīng)的通信變遷序列的操作算子為:。定義8 (相似

27、變遷序列). 兩個可達變遷序列二二二(S),其對應(yīng)的通信變遷為11 1 2 2 2習(xí)=欽)=匕我2,.幾A，客2 =(2)龍，.冷 。戸2相似，記為：丐止，當(dāng)且僅當(dāng)： k ，-j=1,.,k, L(t：)=L(tj2),(£)-()且 G(G)=G(j)。定義9 (對偶變遷序列). 兩個可達變遷序列 G,；2 三(S),其對應(yīng)的通信變遷為1 =；("-”)=：匕，t? ,., tk - , ；2 = ；2)= " L ,上2 ,., t| 。1，”2 互為對偶變遷序列，記為：J 二二，當(dāng)且僅當(dāng)：丨,-j =1,.,k , L(t：)=L(tj2),«)=

28、 -卷2)且 G(J)=G(J)。在定義8和定義9中，變遷的極性函數(shù) Tr 1,0, -1定義為：若變遷t向外界發(fā)送消息，則；：(t)工-1 ;若變遷t從外界接收消息，則：(t 1 ;若變遷t不是通信變遷，則：(t)二0。另外，本文將著色 Petri網(wǎng)定義中的警衛(wèi)(Guard )函數(shù)的定義域從單個變遷集擴展到可達變遷序列集?？蛇_變遷序列的警衛(wèi)函數(shù) G :匕(S)-； BoolExpressio n ,即 1 (S) ,；-： t1,.,tn -:G&)二G(tJ G(tn)。在此基礎(chǔ)上，本文給出兩個服務(wù)流程相似和等價的定義。定義10 (服務(wù)流程相似).給定兩個服務(wù)S、S2，服務(wù)S2的流

29、程與服務(wù)S的流程相似，記為：S2，當(dāng)且僅當(dāng)- ；2%(?2)，M2i二 2M 2，則 T； 二 T(S|)， M；.皿！，匚?。?、；2，并且滿足：(1) 如果 M!二 M1F 或 MJ* M M1F，那么 M2 二 M2F 或 M2 * M2fM2F ；(2) 如果哉久，匕=，使得M M <' M F， M1t1 ，那么Tt2 T2， t2 =,L(t2)=L(tJ，垃2)= 0)，使得 M2【* M2-M2F, M2U2。定義11(服務(wù)流程等價).兩個服務(wù)S和S2的流程等價，記為：SS2，當(dāng)且僅當(dāng)：S > S2如定義10所述，服務(wù)S2的流程與服務(wù)S1的流程相似并不能得出服

30、務(wù)S的流程與服務(wù) S>的流程相似?？梢妰蓚€服務(wù)流程的相似關(guān)系并不滿足對稱性。而定義11所述的服務(wù)流程等價關(guān)系則滿足對 稱性，即：S,、$ = E、3。需要指出的是，根據(jù)定義 10和定義11不難證明服務(wù)流程的相似關(guān)系和等價關(guān)系均滿足傳遞性，即：S1>S2,S2>S3=SS3 ； SftS2,S2fc:S3nS1fc:S3。如前所述，服務(wù)流程的相似性定義需要與上下文無關(guān)。下面將證明給出的定義 10對于良構(gòu)的服務(wù)是上下文無關(guān)的。引理. 設(shè)兩個良構(gòu)的服務(wù) §和S，能夠組合，服務(wù)3和s的流程是相容的，即：sL ，當(dāng)且僅當(dāng)：對于- G*(S), 一二2 二(S2)，M1ipM

31、M1，M2i6 M2，如果從-1 (二 2 )中 去除那些與：二2 (二1 )無關(guān)的通信變遷之后，分別得到變遷序列二1和匚2，二；和匚2互為對偶變遷序列，那么下列兩個條件必有一個滿足：(1) M< M1F 或 MJ* M1f M1F，且 M2 M2F 或 M2* M2f M2F ；(2) b 丁門廣，t2 T2 飛-,L(tJ = L(t2)，(tj 一 ，使得 M* MM1f,M1t1， M2 * M2 ' M2F， M 2t2。證明.記服務(wù)S和S2的組合服務(wù)為S。一方面，如果已知服務(wù) S和S2的流程相容， 0和 2 互為對偶變遷序列，那么此時組合服務(wù) S到達某個可達標(biāo)識 M。

32、如果M是終止標(biāo)識，則MM1F 且M2 M2F。反之，根據(jù)定理 2可知，服務(wù)§和S均沒有到達終止標(biāo)識，并且在標(biāo)識 M下存在 某個變遷可以使能觸發(fā)。因此命題的必要性得證。另一方面，如果二；和匚2互為對偶變遷序列，不妨設(shè)組合服務(wù)S到達某個可達標(biāo)識 M。如果M 不是一個終止標(biāo)識，那么或者 M.* M1 M1F且M2 M2 M2F，或者 帚T,，t .， t2 T2 , t2 =, L(tJ=L(t2), (tj =(t2)，使得 M1 * M < M F1， M1t1,M2:M' M2F，M2& 。無論哪種情況，都可知三:(S)，使得M匸 Mr Mf。根據(jù)定理2可知，命

33、題的充分性得證。證畢.定理3. 設(shè)服務(wù)S,，S,和S是良構(gòu)的，如果 S2>-S1，SL S，那么SL S2。證明.對于 - I (S)，-二2 匕(S,)，Mj二-M，M2i二2 M2，從二(二2)中去除那些與二2 (匚)無關(guān)的通信變遷之后，分別得到變遷序列和二2 , ；和二2互為對偶變遷序列。因為S2 >3，根據(jù)定義10可知，二(SO，M 1i 1 M1，二1 ：、二2。因此，當(dāng)二1中去除那些與 二無關(guān)的通信變遷之后得到的變遷序列匚1，可知匚1和二互為對偶變遷序列。又因為SL S，根據(jù)引理結(jié)論知，M Mf或M * M f Mf，且MM1F或M* M“ M1F ;或者t T， t=

34、 ,1 J，t ，L(t)二L(tJ，(t- (t1)，使得 M* M-Mf，M t ，M1 * MM1F ，皿氐。因為S2 > S ，根據(jù)定義10可知，若M1 皿仆或 M1 *M1f M1F ,則 M2 M2F或M2 * M2f M2F。反之，若 t< T1， t使得M1 *M1M f , M1H1，貝Ut2 T2，t 使得 M2 * M 2 M f , M2H2，且L(t2)=L(tJ , 2) =館)。根據(jù)引理結(jié)論可知，S和S，的流程是相容的，即：sL S2。證畢.定理3的結(jié)論表明，在服務(wù)都是良構(gòu)的前提下，如果某個服務(wù) S,與另一個服務(wù)S相似，那么對于所有與服務(wù)S,流程相容的

35、服務(wù)S，服務(wù)S2與服務(wù)S的流程必然也是相容的。 這一點在進行服務(wù)替換的過程中非常有用。 如果服務(wù)0是某個組合服務(wù)系統(tǒng)中的一個成員服務(wù)，當(dāng)0由于某些原因無法繼續(xù)提供服務(wù)或者無法保證服務(wù)質(zhì)量要求而需要被替換時，只需要找到一個與 0相似的服務(wù)進行替換即可，而不需要再對替換后的組合服務(wù)進行正確性驗證。這是因為定理3的結(jié)論保證了用 S,替換S之后的服務(wù)組合仍然是正確的。由此可見，本文給出的服務(wù)相似性的定義是與上下文無關(guān)的。一些分析服務(wù)相容性的方法用到了“反(opposite)”服務(wù)的概念16。對于一個服務(wù) S，改變其中所有與外部通信庫所關(guān)聯(lián)的弧的方向即可得到服務(wù)S的反服務(wù)，記為 S。可見得到反服務(wù)的操作

36、非常簡單，并且易知一個服務(wù)與其反服務(wù)總是流程相容的，即：SLI S。下面給出與反服務(wù)有關(guān)的兩個結(jié)論。這兩個結(jié)論對已有的基于反服務(wù)概念來分析服務(wù)相容性的方法具有一定應(yīng)用價值。推論1. 設(shè)服務(wù)s和s是良構(gòu)的，服務(wù)s的反服務(wù)為s。如果s > s，那么SiL s。證明.因為sUS，0's，由定理3可知：sLS。證畢.推論2.設(shè)服務(wù)S，S和S是良構(gòu)的，服務(wù)S的反服務(wù)為S。如果S>s，S2S，那么S L S2。證明.因為，由推論i可知：sL S。又因為s，由定理3可知：qL s2。證畢.下面給出一個算法用于判斷兩個Web服務(wù)流程之間是否存在相似關(guān)系，即判斷服務(wù)S的流程是否與服務(wù)S的流程

37、相似。該算法本質(zhì)上需要分別遍歷服務(wù)S1和S2的通信可達樹11，并根據(jù)定義10來判斷是否存在相似性。由于通信可達樹的節(jié)點個數(shù)有限，且通信變遷個數(shù)也有限，因此該算法是 可以終止的。服務(wù)流程相似性判定算法如下：Set T (S, M ); / for all transitions of service S that are enabled in the marking M Set U 2 二 一 ;/ the set of markings of service S2 that has been checkedSet M1 =皿哲，M = M 2i ;IsSimilar ( S2 , S| )1.

38、 if M - M 2fif M M 1F or M1. M1f 三 M1Fthen return TRUE;else return FALSE;2. for each t2 T(S2,M2) and M2 U2if t , M 2 M 2then add M 2 to U2, M2=M2", return IsSimilar ( S2, S )； else M 2t2M 2ifT, t| = , M M1, M1t1 M / ,and L(t2)=L(tJ,(t?)(tjthen if M - M1 f or M1” M1 - M 1fif M2 M2F or M2M2f M2Ft

39、hen return TRUE;else return FALSE;elset；T1,t - , M； * M1(3) ,M1(3)t；Mift2 T2, t , M2I* M2, M2t2M23),and L&) =L(tJ,危)=(tjthen add M 2 to U 2, M 勺=M；4), M 2 = M 2® , return IsSimilar ( S2, S );else return FALSE;else return FALSE;根據(jù)上述判定算法可以判斷得到,步得到，服務(wù) S,和Ss是等價的。圖Rte goodfeSlid ordtfrSlid urili

40、e*Snd inorwy圖3與服務(wù)S等價的服務(wù)£Rd；- orderRec money El I圖4服務(wù)S的反服務(wù)S4圖3所示的服務(wù)S3與圖1所示的服務(wù)S相似。實際上可以進4給出了服務(wù)S的反服務(wù)S4，不難發(fā)現(xiàn)服務(wù) S,與服務(wù)S4是相容的，服務(wù)S3與服務(wù)S4也是相容的，從而驗證了前面得到的結(jié)論。4相關(guān)工作及討論組合服務(wù)流程的正確性驗證是當(dāng)前面向服務(wù)計算領(lǐng)域的一個研究熱點。文獻14以工作流網(wǎng)為基礎(chǔ)，給出了工作流網(wǎng)正確性的定義，即要求同時滿足可終止條件、正確終止條件以及無死變遷條件。 文獻13指出 Web服務(wù)流程正確可以允許流程內(nèi)部存在死變遷，由此提出“弱合理性(weaksoundness

41、) ”概念。文獻17討論了服務(wù)流程相容的三種不同的定義，并指出“完成(completing)相容”能夠正確驗證出所有異步服務(wù)流程死鎖的問題。然而，這些定義并不能完全反映Web服務(wù)基于消息通信以及松散耦合的本質(zhì)特性。由于Petri網(wǎng)適合于對分布式異步系統(tǒng)進行建模，因此許多研究工作均采用Petri網(wǎng)作為服務(wù)流程建模和分析的理論基礎(chǔ)。文獻18給出了一個基于 Petri網(wǎng)的Web服務(wù)模型，提出了 10種不同的服務(wù)組合方式，并指出可以借助Petri網(wǎng)的分析技術(shù)對組合服務(wù)進行驗證。文獻2提出了基于著色Petri網(wǎng)的Web服務(wù)模型，給出了四種主要的組合運算，并討論了這四種組合運算以及組合模型的某些性質(zhì)。文獻

42、6以著色Petri網(wǎng)為基礎(chǔ)提出了面向消息的Web服務(wù)模型，該模型側(cè)重于對Web服務(wù)元消息的描述及其對服務(wù)協(xié)同通信的影響。文獻7提出了一種基于 Petri網(wǎng)的語義 Web服務(wù)自動組合方法，該方法能夠同時考慮服務(wù)的輸入/輸出以及服務(wù)的行為約束。雖然Petri網(wǎng)能夠?qū)M合服務(wù)進行分析和驗證，但是上述研究成果都沒有對此做深入討論，沒有指出具有哪些性質(zhì)的兩個或多個服 務(wù)的流程是相容的。文獻19借助“虹（siphons）”理論研究了基于 Petri網(wǎng)模型的 Web服務(wù)流程相 容性。然而，上述研究工作大都沒有涉及到服務(wù)流程的相似性和等價性分析。服務(wù)流程相似性分析是與相容性分析密切相關(guān)的一個問題。文獻15提到

43、了研究服務(wù)流程相似和等價的必要性，區(qū)分了服務(wù)發(fā)現(xiàn)和服務(wù)替換兩種不同應(yīng)用背景下的相似性定義，但是作者沒有討論 相似性與相容性之間的關(guān)系，也沒有分析所給出的相似性定義在進行服務(wù)替換時是否與上下文無關(guān)。執(zhí)行路徑（trace）相似和互模擬（bisimulation ）相似是異步并發(fā)系統(tǒng)行為相似性研究中兩個最常用 的概念20。但是這兩個概念并不能完全反映Web服務(wù)流程相容的特性和需求。執(zhí)行路徑相似的要求過于寬松，而互模擬相似的要求則過于苛刻21。文獻16主要研究兩個服務(wù)流程的相容性和可替換性（substitutability ）。作者借助標(biāo)記變遷系統(tǒng)（LTS）對Web服務(wù)的行為進行建模，提出了三個不同

44、概念意義下的相容性定義，并相應(yīng)的給出了三種不同的可替換性定義，同時指出可替換性定義分為 與上下文相關(guān)和與上下文無關(guān)兩種。但是作者并沒有深入討論與上下文無關(guān)的可替換性需要滿足的 充分條件。文獻5采用進程代數(shù)建模 Web服務(wù)流程，給出了與上下文無關(guān)的服務(wù)流程一致性的定義 及其驗證算法。作者指出Web服務(wù)需要為每種接收到的消息類型設(shè)置緩存區(qū)，然而基于進程代數(shù)的方法無法顯式的建模這些消息緩存區(qū)。文獻22使用Martin類型論（Martin Type Theory, MTT ）建模Web服務(wù)行為，研究了 Web服務(wù)行為一致性與相容性的判定方法。然而，但是基于進程代數(shù)或 MTT的方法并不能對服務(wù)的內(nèi)部選擇

45、操作進行精細的刻畫，也無法建模和分析 Web服務(wù)的結(jié)構(gòu)性質(zhì)（如:良構(gòu)性等）。上述相關(guān)工作為本文展開服務(wù)流程相容性和相似性研究提供了很好的啟示和基礎(chǔ)。與之相比， 本文研究工作的特色在于：1 ）采用著色Petri網(wǎng)建模 Web服務(wù)流程，該模型能夠?qū)Ψ?wù)流程的消息緩存區(qū)和內(nèi)部選擇操作進行精細的刻畫，較其他建模方法更為直觀。在此基礎(chǔ)上給出了服務(wù)流程正 確性的定義，該定義允許服務(wù)流程正確結(jié)束時其內(nèi)部或外部消息緩存區(qū)（也即通信庫所）中留有未 被消耗的消息。與現(xiàn)有正確性定義相比，該定義的要求更為寬松，更符合Web服務(wù)基于消息通信、松散耦合的本質(zhì)特性；2）分析了 Web服務(wù)的結(jié)構(gòu)性質(zhì)，提出了 Web服務(wù)良構(gòu)性

46、的概念，并指出成 員服務(wù)的良構(gòu)性有效的保證了組合服務(wù)可達終止標(biāo)識的正確性，從而簡化了服務(wù)流程相容性分析的 條件；3）基于著色Petri網(wǎng)模型提出了服務(wù)流程相似性的定義，該定義考慮了服務(wù)流程的內(nèi)部選擇操作。證明了該定義在進行服務(wù)替換時是與上下文無關(guān)的，并且討論了服務(wù)流程相似性與相容性之 間的關(guān)系。5結(jié)束語在服務(wù)組合驗證研究中，服務(wù)流程的相容性和相似性分析是兩個密切相關(guān)的問題，具有較大的 實用價值。本文采用著色Petri網(wǎng)建模 Web服務(wù)的流程，給出了服務(wù)流程正確性的定義，并在此基礎(chǔ)上定義了服務(wù)流程的相容性。提出了服務(wù)良構(gòu)性的概念，并指出成員服務(wù)的良構(gòu)性能夠保證組合 服務(wù)可達終止?fàn)顟B(tài)是正確的，從而

47、簡化了相容性分析的條件。在服務(wù)流程相似性分析方面，本文給 出了相似性的定義，證明了滿足相似關(guān)系的兩個服務(wù)在進行替換時是上下文無關(guān)的，并給出了相似 性判定算法。本文工作對于研究服務(wù)發(fā)現(xiàn)、服務(wù)組合和服務(wù)替換具有重要參考價值。未來工作主要在三個方面展開：1)本文中相似性判定算法的復(fù)雜度隨通信可達樹節(jié)點個數(shù)呈指數(shù)增長，未來將考慮采用穩(wěn)固集( stubborn sets)的方法提高算法在產(chǎn)生狀態(tài)空間方面的性能；2)將研究當(dāng)兩個 Web服務(wù)的流程不完全相容時，是否可以通過產(chǎn)生中介器( mediator)來幫助兩者實 現(xiàn)流程相容。目前學(xué)術(shù)界針對該問題已經(jīng)有了一些研究成果，但是還沒有一個系統(tǒng)化的解決辦法；3)

48、本研究組正在開發(fā)和完善一套Web服務(wù)組合工具，以便自動化或半自動化的實現(xiàn)服務(wù)流程的建模、組合以及相容性和相似性分析。參考文獻1 Han Yan-Bo, Wang Hong-Cui, Wang Jian-Wu, et al. An end-user-oriented approach to exploratory service composition.Journal of Computer Research and Development, 2006, 43(11): 18951903 (in Chinese)(韓燕波，王洪翠，王建武等.一種支持最終用戶探索式組合服務(wù)的方法.計算機研究與發(fā)展，

49、2006, 43(11):18951903)2 Guo Yu-Bin, Du Yu-Y ue, Xi Jian-Qing. A CP-net model and operation properties for Web service composition. ChineseJournal of Computers, 2006, 29(7): 10671075 (in Chinese)(郭玉彬，杜玉越，奚建清.Web服務(wù)組合的有色網(wǎng)模型及運算性質(zhì).計算機學(xué)報，2006, 29(7): 10671075)3 Foster H., Uchitel S., Kramer J. et al. Comp

50、atibility verification for web service choreography. In: Proceedings of theIEEE Intl. Conf. on Web Services, San Diego, CA, USA, 2004, 738741.4 Deng Shui-Guang, Li Ying, Wu Jian, et al. Determination and computation of behavioral compatibility for Web services. Journal of Software, 2007, 18(12): 300

51、13014 (in Chinese)(鄧水光，李瑩，吳健等.Web服務(wù)行為兼容性的判定與計算.軟件學(xué)報，2007, 18(12): 30013014)5 Liu Fang-Fang, Shi Yu-Liang, Zhang Liang, et al. Substitution analysis of Web service composition via process algebra.Chinese Journal of Computers, 2007, 30(11): 20332039 (in Chinese)(劉方方，史玉良，張亮等.基于進程代數(shù)的 Web服務(wù)合成的替換分析.計算機學(xué)報，

52、2007, 30(11): 20332039)6 Qian Zhu-zhong, Lu Sang-Lu, Xie Li. Automatic composition of Petri net based Web services. Chinese Journal of Computers, 2006, 29(7): 10571066 (in Chinese)(錢柱中，陸桑璐，謝立.基于Petri網(wǎng)的Web服務(wù)自動組合研究.計算機學(xué)報，2006, 29(7): 10571066)7 Tang Xian-Fei, Jiang Chang-Jun, Ding Zhi-Jun, et al. A Pe

53、tri net-based semantic Web service automatic composition method. Journal of Software, 2007, 18(12): 29913000 (in Chinese)(湯憲飛，蔣昌俊，丁志軍等.基于Petri網(wǎng)的語義 Web服務(wù)自動組合方法.軟件學(xué)報，2007, 18(12): 29913000)8 Hu Chun-Hua, Wu Min, Liu Guo-Peng. QoS scheduling based on trust relationship in Web service workflow. Chinese

54、Journal of Computers, 2009, 32(1): 4253 (in Chinese)(胡春華，吳敏，劉國平.Web服務(wù)工作流中基于信任關(guān)系的QoS調(diào)度.計算機學(xué)報，2009, 32(1): 4253)9 Jensen K. Coloured Petri nets: basic concepts, analysis methods and practical use. Vol. 1. Berlin, Heidelberg, New York: Springer-Verlag, 1997.10 Ouyang C., Verbeek E., van der Aalst W.M.P

55、., et al. Formal semantics and analysis of control flow in WS-BPEL. Science of Computer Programming, 2007, 67(2-3):162198.11 Tan W., Fan Y.S., Zhou M.C. A Petri net-based method for compatibility analysis and composition of Web services in business process execution language. IEEE Transactions on Au

56、tomation Science and Engineering, 2009, 6(1): 94106.12 Li Xi-Tong, Fan Yu-Shun. Modeling and logical correctness verification of Web service processes. Computer Integrated Manufacturing Systems, 2008, 14(4): 675682 (in Chinese)(李喜彤，范玉順.Web服務(wù)過程建模及其邏輯正確性驗證.計算機集成制造系統(tǒng)，2008, 14(4): 675682)13 Martens A. On compatibility of Web services. Petri Net Newsletter, 2003, 1220.14 van der Aalst, W.M.P. Workflow verification: finding control-flow errors using Petri net-based techniques. Bu