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

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

2、；服務(wù)組合；服務(wù)替換；相容性；相似性 中圖法分類號(hào) 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收稿日期：修改稿收到日期：本課題得到國(guó)家自然科學(xué)基金(60674080, 60704027)、國(guó)家“八六三”高技術(shù)研究發(fā)展計(jì)劃項(xiàng)目基金(2007AA04Z150)資助。李喜彤，男,1982年生，博士研究生，研究方向?yàn)?Web服務(wù)、面向服務(wù)計(jì)算、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)最流行的一種實(shí)現(xiàn)形式。單個(gè)Web服務(wù)通常無(wú)法滿足用戶需求，而需要將若干個(gè) Web服務(wù)組合起來(lái)協(xié)同工作。服務(wù)組

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

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

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

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

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

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

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

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

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

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

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

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

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

21、合。在工作流網(wǎng)“良構(gòu)性”orderoSnd moneyEM取i; jj.ni.'MR2Sfkl irJcr圖1 一個(gè)良構(gòu)的服務(wù)3morwyUser info圖2 一個(gè)非良構(gòu)的服務(wù) S2定義的基礎(chǔ)上14，本文提出Web服務(wù)良構(gòu)性的定義。定義6 (服務(wù)良構(gòu)性). 服務(wù)S是良構(gòu)的，當(dāng)且僅當(dāng)S對(duì)應(yīng)的工作流網(wǎng)N = ：(S)是良構(gòu)的。根據(jù)上述定義，易知圖1所示的服務(wù)S,是良構(gòu)的，而圖2所示的服務(wù)S2則是非良構(gòu)的。下面給出一個(gè)關(guān)于良構(gòu)的Web服務(wù)及其組合的重要結(jié)論。定理1.設(shè)兩個(gè)服務(wù)S,和S能夠組合，其組合服務(wù)。如果服務(wù)S、S2是良構(gòu)的，那么服務(wù)S從初始標(biāo)識(shí)可達(dá)的任一終止標(biāo)識(shí)都是正確的，即：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存在某個(gè)可 達(dá)的終止標(biāo)識(shí) M使得Mg)工0且Mif(p)羊0。因?yàn)榉?wù)S,對(duì)應(yīng)的工作流網(wǎng) 口=(S)是 強(qiáng)連通的，那么網(wǎng) N,中存在一條從i,到o,的基本路徑 G使得p - G，并且存在一

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

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

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

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

27、變遷序列). 兩個(gè)可達(dá)變遷序列二二二(S),其對(duì)應(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 (對(duì)偶變遷序列). 兩個(gè)可達(dá)變遷序列 G,；2 三(S),其對(duì)應(yīng)的通信變遷為1 =；("-”)=：匕，t? ,., tk - , ；2 = ；2)= " L ,上2 ,., t| 。1，”2 互為對(duì)偶變遷序列，記為：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ù)的定義域從單個(gè)變遷集擴(kuò)展到可達(dá)變遷序列集?？蛇_(dá)變遷序列的警衛(wèi)函數(shù) G :匕(S)-； BoolExpressio n ,即 1 (S) ,；-： t1,.,tn -:G&)二G(tJ G(tn)。在此基礎(chǔ)上，本文給出兩個(gè)服務(wù)流程相似和等價(jià)的定義。定義10 (服務(wù)流程相似).給定兩個(gè)服務(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ù)流程等價(jià)).兩個(gè)服務(wù)S和S2的流程等價(jià)，記為：SS2，當(dāng)且僅當(dāng)：S > S2如定義10所述，服務(wù)S2的流程與服務(wù)S1的流程相似并不能得出服

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

31、M1，M2i6 M2，如果從-1 (二 2 )中 去除那些與：二2 (二1 )無(wú)關(guān)的通信變遷之后，分別得到變遷序列二1和匚2，二；和匚2互為對(duì)偶變遷序列，那么下列兩個(gè)條件必有一個(gè)滿足：(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 互為對(duì)偶變遷序列，那么此時(shí)組合服務(wù) S到達(dá)某個(gè)可達(dá)標(biāo)識(shí) M。

32、如果M是終止標(biāo)識(shí)，則MM1F 且M2 M2F。反之，根據(jù)定理 2可知，服務(wù)§和S均沒有到達(dá)終止標(biāo)識(shí)，并且在標(biāo)識(shí) M下存在 某個(gè)變遷可以使能觸發(fā)。因此命題的必要性得證。另一方面，如果二；和匚2互為對(duì)偶變遷序列，不妨設(shè)組合服務(wù)S到達(dá)某個(gè)可達(dá)標(biāo)識(shí) M。如果M 不是一個(gè)終止標(biāo)識(shí)，那么或者 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& 。無(wú)論哪種情況，都可知三:(S)，使得M匸 Mr Mf。根據(jù)定理2可知，命

33、題的充分性得證。證畢.定理3. 設(shè)服務(wù)S,，S,和S是良構(gòu)的，如果 S2>-S1，SL S，那么SL S2。證明.對(duì)于 - I (S)，-二2 匕(S,)，Mj二-M，M2i二2 M2，從二(二2)中去除那些與二2 (匚)無(wú)關(guān)的通信變遷之后，分別得到變遷序列和二2 , ；和二2互為對(duì)偶變遷序列。因?yàn)镾2 >3，根據(jù)定義10可知，二(SO，M 1i 1 M1，二1 ：、二2。因此，當(dāng)二1中去除那些與 二無(wú)關(guān)的通信變遷之后得到的變遷序列匚1，可知匚1和二互為對(duì)偶變遷序列。又因?yàn)镾L 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 ，皿氐。因?yàn)镾2 > 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)的前提下，如果某個(gè)服務(wù) S,與另一個(gè)服務(wù)S相似，那么對(duì)于所有與服務(wù)S,流程相容的

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

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

37、相似。該算法本質(zhì)上需要分別遍歷服務(wù)S1和S2的通信可達(dá)樹11，并根據(jù)定義10來(lái)判斷是否存在相似性。由于通信可達(dá)樹的節(jié)點(diǎn)個(gè)數(shù)有限，且通信變遷個(gè)數(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是等價(jià)的。圖Rte goodfeSlid ordtfrSlid urili

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

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

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

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

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

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

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

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

48、本研究組正在開發(fā)和完善一套Web服務(wù)組合工具，以便自動(dòng)化或半自動(dòng)化的實(shí)現(xiàn)服務(wù)流程的建模、組合以及相容性和相似性分析。參考文獻(xiàn)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ù)的方法.計(jì)算機(jī)研究與發(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)模型及運(yùn)算性質(zhì).計(jì)算機(jī)學(xué)報(bào)，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ù)行為兼容性的判定與計(jì)算.軟件學(xué)報(bào)，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)(劉方方，史玉良，張亮等.基于進(jìn)程代數(shù)的 Web服務(wù)合成的替換分析.計(jì)算機(jī)學(xué)報(bào)，

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ù)自動(dòng)組合研究.計(jì)算機(jī)學(xué)報(bào)，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)的語(yǔ)義 Web服務(wù)自動(dòng)組合方法.軟件學(xué)報(bào)，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)(胡春華，吳敏，劉國(guó)平.Web服務(wù)工作流中基于信任關(guān)系的QoS調(diào)度.計(jì)算機(jī)學(xué)報(bào)，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ù)過(guò)程建模及其邏輯正確性驗(yàn)證.計(jì)算機(jī)集成制造系統(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