胡曉靜，劉士喜，王　濤

(滁州學(xué)院 計算機與信息工程學(xué)院，安徽 滁州 239000)

一種Web服務(wù)組合模型合理性驗證方法

胡曉靜，劉士喜，王濤

(滁州學(xué)院 計算機與信息工程學(xué)院，安徽 滁州 239000)

摘要:為了更加有效地對Web服務(wù)組合進(jìn)行分析驗證，設(shè)計BPEL到PNML語言的文件轉(zhuǎn)換規(guī)則，實現(xiàn)Web服務(wù)組合流程的Petri網(wǎng)建模。針對Web服務(wù)組合流程設(shè)計中可能存在死鎖及不正確的流程，在不破壞原Petri網(wǎng)模型結(jié)構(gòu)性質(zhì)與系統(tǒng)行為的基礎(chǔ)上，將其調(diào)整映射為自由選擇網(wǎng)。在自由選擇Petri網(wǎng)理論基礎(chǔ)上，設(shè)計了一種Web服務(wù)組合Petri網(wǎng)模型的合理性驗證規(guī)則，能在多項式時間內(nèi)分析網(wǎng)模型的結(jié)構(gòu)活性與有界性，從而避免采用傳統(tǒng)的可達(dá)樹等分析方法出現(xiàn)的狀態(tài)空間爆炸問題。最后，使用兩個具體的Web服務(wù)組合Petri網(wǎng)模型證明了本文方法的有效性。

關(guān)鍵詞：Web服務(wù)； Petri網(wǎng)；合理性驗證；自由選擇網(wǎng)

中圖分類號：TP311

文獻(xiàn)標(biāo)志碼：碼：A

文章編號：號：2095-4824(2015)03-0016-05

收稿日期：2015-02-12

基金項目：安徽省高校省級科學(xué)研究項目(KJ2012Z282)；滁州學(xué)院自然科學(xué)基金資助項目(2011kj008B)；滁州學(xué)院科研啟動基金項目(2012qd09)；安徽省自然科學(xué)基金項目(1508085MF123)

作者簡介：胡曉靜(1985-)，女，安徽長豐人，滁州學(xué)院計算機與信息工程學(xué)院講師，碩士。

Abstract：To analyze and verify the Web Service composition model more effectively, a file transformation rule from the BPEL files to the PNML is designed for establishing the Petri net model of Web Service composition process. In order to detect the deadlock and wrong process of Web Service composition process, the Petri net model is adjusted and mapped to Free Choice net, which is based on the premise that it would not affect the constitutive property and system behavior of the original model. Combining the Commoner theorem with the rank theorem, this paper proposes a rationality verification approach for the Web service composition model, and analyses the structural liveliness and rationality of Free Choice net in polynomial time. Finally, two specific Web Services composition Petri net models are employed to verify the effectiveness of the proposed method.

劉士喜(1982-)，男，安徽淮南人，滁州學(xué)院計算機與信息工程學(xué)院講師，碩士。

王濤(1979-)，男，山東淄博人，滁州學(xué)院計算機與信息工程學(xué)院講師，博士。

在Web服務(wù)組合建模階段，組合服務(wù)流程可能存在死鎖、不可達(dá)等問題，因此建立邏輯正確、結(jié)構(gòu)合理的Web組合流程是Web服務(wù)組合成功執(zhí)行的關(guān)鍵。Web服務(wù)組合流程合理性驗證目的在于對建模階段所得到的服務(wù)組合模型進(jìn)行動態(tài)行為、結(jié)構(gòu)性質(zhì)的分析，發(fā)現(xiàn)其中的異常結(jié)構(gòu)(如死語句、死鎖等)，保證組合服務(wù)在執(zhí)行前的正確性。BPEL、XLANG、WSFL和WCSI等是主要的Web服務(wù)組合流程建模語言[1]。Petri網(wǎng)以其圖形化的表現(xiàn)形式、眾多的分析方法和堅實的數(shù)學(xué)基礎(chǔ)，成為研究Web服務(wù)組合的重要建模工具之一。合理性概念最早是Aalst提出的，用于判斷工作流Petri網(wǎng)的有效性和正確性，他提出當(dāng)且僅當(dāng)該網(wǎng)系統(tǒng)是活的而且是有界時，工作流網(wǎng)是合理的[2]。Web服務(wù)組合Petri網(wǎng)與工作流Petri網(wǎng)類似，判斷Web服務(wù)組合Petri網(wǎng)的合理性，其本質(zhì)就是分析該網(wǎng)模型的活性和有界性?；钚院陀薪缧允荘etri網(wǎng)的重要性質(zhì)之一，與被模擬的系統(tǒng)的無死鎖性密切相關(guān)[3]。

Petri網(wǎng)的可達(dá)樹方法是判斷Petri網(wǎng)活性和有界性等特性的重要分析方法之一[4]。然而，采用可達(dá)樹分析方法對于復(fù)雜的Petri網(wǎng)的分析能力不足，容易導(dǎo)致狀態(tài)空間爆炸等問題。綜合國內(nèi)外研究現(xiàn)狀，目前只有Petri網(wǎng)的特殊子類，例如自由選擇網(wǎng)才能夠有效求解網(wǎng)模型的活性和有界性，以避免狀態(tài)空間爆炸等問題。Balbo等[5]提出在自由選擇網(wǎng)條件下分析工作流Petri網(wǎng)合理性的定理。Desel等[6]給出了Commoner定理和Rank定理，使得不使用可達(dá)樹、關(guān)聯(lián)矩陣和狀態(tài)方程等傳統(tǒng)方法，而采用多項式方法求解自由選擇網(wǎng)的活性與有界性。很多學(xué)者基于Desel等的理論，采用多項式方法判斷自由選擇網(wǎng)的活性和有界性。Kemper等[7]給出了在多項式時間內(nèi)求解自由選擇網(wǎng)有界性與活性的算法。文獻(xiàn)[8]結(jié)合Commoner定理和Rank定理給出如何獲取最小死鎖的算法，但未給出求解最小死鎖的具體過程和實例驗證。文獻(xiàn)[9]采用BPEL語言進(jìn)行Web服務(wù)組合建模，通過PNML + OWL 描述自動得到Web 服務(wù)組合Petri 網(wǎng)的方法，從而實現(xiàn)Petri網(wǎng)的建模。

在借鑒Petri網(wǎng)和自由選擇網(wǎng)理論的活性、有界性研究成果的基礎(chǔ)上，本文采用BPEL4WS語言描述Web服務(wù)流程，設(shè)計了BPEL到PNML語言的文件轉(zhuǎn)換規(guī)則，實現(xiàn)Web服務(wù)組合流程的Petri網(wǎng)建模。通過將Petri網(wǎng)調(diào)整為自由選擇網(wǎng)，結(jié)合自由選擇網(wǎng)中的Commoner定理和Rank定理，給出組合流程合理性驗證規(guī)則，采用多項式的方式分析網(wǎng)模型的活性及有界性，避免傳統(tǒng)可達(dá)樹等方法帶來的狀態(tài)空間爆炸等問題，以簡化模型求解的復(fù)雜性。最后，以網(wǎng)系統(tǒng)模型驗證該方法的有效性。

1　Web服務(wù)組合的Petri網(wǎng)建模

BPEL4WS是為整合現(xiàn)有Web服務(wù)而制定的一項規(guī)范標(biāo)準(zhǔn)，其目的在于將一組現(xiàn)有的Web服務(wù)組合起來，定義一個新的Web服務(wù)。

在BPEL文檔中，invoke代表一個Web服務(wù)，name是Web服務(wù)名稱，operation 代表Web服務(wù)操作，input variable 代表Web服務(wù)的輸入，output variable 代表Web服務(wù)的輸出。在Petri網(wǎng)模型中，庫所(Place)與Web服務(wù)的發(fā)生前后相對應(yīng)，變遷(Transition)對應(yīng)著Web服務(wù)的活動，標(biāo)記(Token)對應(yīng)著服務(wù)的狀態(tài)，Petri網(wǎng)的弧(Arc)對應(yīng)服務(wù)流程的關(guān)系。

為了實現(xiàn)BPEL文件的Petri網(wǎng)建模，需要借助PNML語言。PNML是一種基于XML的Petri網(wǎng)標(biāo)記語言，是獨立于工具和平臺的Petri網(wǎng)文件交換標(biāo)準(zhǔn)。由于BPEL文件與PNML文件都是基于XML語言描述的，因此編寫XSLT轉(zhuǎn)換文件，設(shè)計BPEL到PNML語言的文件轉(zhuǎn)換規(guī)則，可實現(xiàn)BPEL文件的Petri網(wǎng)建模。

下面以BPEL中常見的sequence流程為例，說明BPEL到PNML的文件轉(zhuǎn)換規(guī)則。

⑴ 編寫XSLT文檔，匹配BPEL文件中的process/sequence元素，生成PNML文件的和。

⑵ 分別建立sequence、invoke元素模板，生成Petri網(wǎng)的變遷(transition)與弧，生成Petri網(wǎng)的輸入、輸出庫所()。

⑶ 獲取invoke的屬性operation值，生成變遷(transition)的名稱。生成庫所與變遷之間的連接弧，利用position()函數(shù)生成連接弧(arc)的起始對象(source)和指向?qū)ο?target)。

⑷利用position()函數(shù)為PNML文件中的每個元素生成圖形信息()。將已經(jīng)生成的PNML文件導(dǎo)入Petri網(wǎng)建模工具，即可完成Web服務(wù)組合的Petri網(wǎng)圖形化建模[10]。

基于BPEL語言描述的Web服務(wù)組合Petri網(wǎng)模型的定義如下：

定義1BPEL-PN是一個基本Petri網(wǎng)：N=(P,T; F) ，其中：

⑴ P={p1,p2,……pm}是庫所的有限集，代表BPEL4WS流程的發(fā)生前條件與發(fā)生后條件。

⑵ T={t1,t2,……tn}是變遷的有限集，代表BPEL4WS流程的動作。

⑶ F?P×T∪T×P是BPEL流程動作流關(guān)系的有限集。

結(jié)合工作流網(wǎng)的合理性研究理論，給出BPEL-PN合理性的形式化定義以及判定定理。

定義2BPEL-PN：N=(P,T; F)模型是合理的，當(dāng)且僅當(dāng)：

⑴ 對于初始標(biāo)識Mi(庫所i包含一個Token的標(biāo)識)可達(dá)的每一個標(biāo)識M，存在一個啟動順序使得標(biāo)識M可達(dá)標(biāo)識M0, 即 ?M(Mi[*>M→M[*>M0)。

⑵ 標(biāo)識Mj(庫所j包含一個Token標(biāo)識)是從初始標(biāo)識可達(dá)，則Mj是唯一滿足庫所j至少包含一個Token的標(biāo)識，?M (Mj[*>M∧M≥Mj) →M=Mj。

⑶ 在(N, Mi)中不存在死的轉(zhuǎn)移，?t∈T ?M,M’ , Mj[*>M[t> M’。

Web服務(wù)組合Petri網(wǎng)的合理性與Petri網(wǎng)的結(jié)構(gòu)活性和有界性密切相關(guān)，結(jié)合文獻(xiàn)[1]給出以下結(jié)論。

定理1BPEL-PN網(wǎng)是合理的，當(dāng)且僅當(dāng)該網(wǎng)系統(tǒng)N=(P,T; F,Mi)是活的且有界的。

2　BPEL-PN的合理性驗證

不合理的Web服務(wù)組合流程大多是服務(wù)不正確的調(diào)用或流程內(nèi)部節(jié)點不正確的連接造成的。Web服務(wù)組合流程不合理性主要表現(xiàn)在：流程結(jié)構(gòu)混亂、Petri網(wǎng)模型中存在無界的庫所或發(fā)生序列、存在死變遷與不活的變遷或變遷發(fā)生序列。大多數(shù)有效求解一個網(wǎng)模型活性和有界性的算法都是建立在自由選擇網(wǎng)的基礎(chǔ)上。對于比較復(fù)雜的系統(tǒng)模型，一般也是將其轉(zhuǎn)化為自由選擇網(wǎng)后進(jìn)行分析。本文提出的Web服務(wù)組合合理性驗證過程如圖1所示。

圖1　合理性驗證過程

2.1　模型調(diào)整

在BPEL-PN網(wǎng)中，不符合自由選擇網(wǎng)結(jié)構(gòu)主要有兩種結(jié)構(gòu)類型，分別是反饋結(jié)構(gòu)和不平衡結(jié)構(gòu)[8]。對于反饋結(jié)構(gòu)，在Petri網(wǎng)中存在某個叢，同時有該叢的庫所P到變遷T的有向弧和從變遷T到庫所P的有向弧(見圖2)。對不平衡結(jié)構(gòu)[8]，Petri網(wǎng)中存在庫所P和變遷T，滿足[P]=[T]，并且(P,T)不是Petri網(wǎng)中的有向不是Petri網(wǎng)中的有向弧(見圖3)。

圖2反饋結(jié)構(gòu)圖3不平衡結(jié)構(gòu)

定義映射φ1和φ2，將不符合自由選擇網(wǎng)的Petri模型調(diào)整為(擴展)自由選擇網(wǎng)。由于網(wǎng)的叢是有限的，因此經(jīng)過有限步的調(diào)整后，可以把Petri網(wǎng)調(diào)整為自由選擇網(wǎng)。調(diào)整后的網(wǎng)系統(tǒng)與原網(wǎng)具有相同的結(jié)構(gòu)活性和結(jié)構(gòu)有界性，這種調(diào)整不會改變系統(tǒng)的結(jié)構(gòu)特性[6]。

定義3[8]令N是一個BPEL4-PN，映射φ1(N)定義為對N中每個反饋結(jié)構(gòu)移去弧(t,p)，增加新的庫所 p’和新的變遷t’，增加新的弧(t,p’)、(p’,t’)和(t’,p)。反饋結(jié)構(gòu)調(diào)整過程如圖4所示。映射φ1(N)定義為對N中的每個不平衡結(jié)構(gòu)增加新的弧(p,t)和(t,p)。不平衡結(jié)構(gòu)調(diào)整過程如圖5所示。

圖4　反饋結(jié)構(gòu)調(diào)整

圖5　不平衡結(jié)構(gòu)調(diào)整

2.2　合理性驗證

將Petri網(wǎng)模型經(jīng)過有限次映射后調(diào)整為自由選擇網(wǎng)，構(gòu)造該網(wǎng)模型的求解合理性算法。在提出Web服務(wù)組合的合理性定理前，引入兩個與自由選擇網(wǎng)的活性和有界性有關(guān)的定理。

定義4[6]設(shè)X是網(wǎng)N=(P,T; F)節(jié)點的集合，[X]表示X的叢，當(dāng)且僅當(dāng)滿足下列條件：

⑴ X∈[X]；

⑵ 如果庫所p∈[X]，則也有p·∈[X]；

⑶ 如果變遷t∈[X]，則也有·t∈[X]。

定義5[11]虹吸 N= (P, T; F)為一個Petri網(wǎng)，一個非空集合S?P是虹吸當(dāng)且僅當(dāng)·S?S·。

定義6[11]陷阱 N= (P, T; F)為一個Petri網(wǎng)，一個非空集合S?P是陷阱當(dāng)且僅當(dāng)S·?S·。

定理2[6]Commoner定理 自由選擇網(wǎng)系統(tǒng)(N, M0)是活的，當(dāng)且僅當(dāng)網(wǎng)系統(tǒng)的每一個虹吸都包含一個被M0標(biāo)識的陷阱。

定理3[6]Rank定理 (擴展)自由選擇網(wǎng)N=(P,T; F)是結(jié)構(gòu)有界且結(jié)構(gòu)活的，當(dāng)且僅當(dāng)滿足以下條件：

⑴ N存在正的P-不變量；

⑵ N存在正的T-不變量；

⑶ |A| = Rank(N) + 1，其中Rank(N)是網(wǎng)N關(guān)聯(lián)矩陣的秩，A是網(wǎng)N的叢集合。

根據(jù)Petri網(wǎng)結(jié)構(gòu)有界和Petri網(wǎng)系統(tǒng)有界性定義及性質(zhì)，一個Petri網(wǎng)是結(jié)構(gòu)有界的，則該Petri網(wǎng)系統(tǒng)也必然是有界的[3]。因此，當(dāng)一個自由選擇網(wǎng)滿足定理2與定理3，其必然是結(jié)構(gòu)有界并且活的。本文在以上定理的基礎(chǔ)上，給出BPEL-PN網(wǎng)系統(tǒng)的合理性判斷定理。

定理4BPEL-PN合理性 Web服務(wù)組合Petri網(wǎng)系統(tǒng)(N,Mi)是合理的，當(dāng)且僅當(dāng)調(diào)整后的(擴展)自由選擇網(wǎng)(N’,Mi’)：

⑴ N’有正的S-不變量；

⑵ N’有正的T-不變量；

⑶ |C N’| = Rank(N’) + 1

⑷ 網(wǎng)系統(tǒng)每個虹吸都包含一個被Mi’標(biāo)識的陷阱。

定理5[2]設(shè)N=(P,T;F)為一個網(wǎng)，C為N的關(guān)聯(lián)矩陣。p1={pi1,pi2,……pik}為網(wǎng)的一個虹吸(陷阱)的充分必要條件是：C關(guān)于P1列的列生成子陣中，每個非全零行至少包含一個“-1”或“1”元素。

3　模型驗證

以兩個具體的Web服務(wù)組合Petri網(wǎng)模型，驗證BPEL-PN合理性判斷定理是否有效。圖6是通過映射φ2調(diào)整后的擴展自由選擇網(wǎng)。

圖6　調(diào)整后的網(wǎng)模型

根據(jù)合理性定理，判斷該模型的合理性步驟如下：

⑴ 根據(jù)擴展自由選擇網(wǎng)的定義，調(diào)整后的網(wǎng)模型是一個擴展自由選擇網(wǎng)。

⑵ 求解此網(wǎng)的關(guān)聯(lián)矩陣C，對關(guān)聯(lián)矩陣C進(jìn)行行初等變換，變換成階梯矩陣求關(guān)聯(lián)矩陣的秩。

⑶階梯矩陣中有3行元素不全為零，因此Rank(N)=3。根據(jù)叢的定義，該網(wǎng)叢的集合為A={(p1,t1),(p2,p3,t2,t3),(p4)} ，叢的集合個數(shù)為3，不符合BPEL-PN合理性定理。

⑷ 根據(jù)定理5計算，網(wǎng)的虹吸有{p1,p2}，{p1,p2,p3}，{p1,p2,p4}。陷阱為{p2,p4}不符合BPEL-PN合理性定理。

⑸ 根據(jù)合理性定理判斷該網(wǎng)是不合理的。

圖7是一個經(jīng)過映射φ1與φ2調(diào)整后的Web服務(wù)組合Petri網(wǎng)模型。

圖7　擴展自由選擇網(wǎng)模型

根據(jù)合理性定理，判斷該模型的合理性步驟如下：

⑴ 根據(jù)擴展自由選擇網(wǎng)的定義，該模型是一個擴展自由選擇網(wǎng)。

⑵ 求解此網(wǎng)的關(guān)聯(lián)矩陣C。對關(guān)聯(lián)矩陣C進(jìn)行行初等變換，化成階梯矩陣求關(guān)聯(lián)矩陣的秩。

⑶ 階梯矩陣中有5行元素不全為零，因此Rank(N)=5。根據(jù)叢的定義，該網(wǎng)叢的集合為A={(p1,t1,t2,p2),(p3,t3),(p4,t4),(p5,t5),(p6,t6),(p7,t7,p8)} ，叢的集合個數(shù)為6，符合BPEL-PN合理性定理。

⑷ 求解此網(wǎng)的一個P-不變量與T-不變量，其中(1,1,1,1,1,1,1,1)是一個正的P-不變量，(1,1,1,1,1,1,2)是一個正的T-不變量。

⑸根據(jù)定理5計算，上述網(wǎng)的虹吸有{p1,p3,p4，p5,p6,p7}，{p1,p3,p4，p5,p6,p8}，{p2,p3,p4，p5,p6,p7}，{p2,p3,p4,p5,p6,p8}。陷阱為{p1,p3,p5，p7,p8},{p1,p4,p5，p7,p8}，{p1,p3,p6，p7,p8}，{p1,p4,p6，p7,p8}，{p2,p3,p5，p7,p8}，{p2,p4,p5，p7,p8}，{p2,p3,p6，p7,p8}，{p2,p4,p6，p7,p8}，網(wǎng)的每個虹吸都包含一個被標(biāo)識的陷阱，符合BPEL-PN合理性定理。

⑹根據(jù)合理性定理，可以判斷該網(wǎng)結(jié)構(gòu)是合理的。

4　結(jié)束語

在Petri網(wǎng)和自由選擇網(wǎng)理論的活性、有界性研究成果的基礎(chǔ)上，采用BPEL語言組合Web服務(wù)，設(shè)計了從BPEL到PNML語言的文件轉(zhuǎn)換規(guī)則，實現(xiàn)了Web服務(wù)組合的Petri網(wǎng)建模。在自由選擇Petri網(wǎng)已有的理論基礎(chǔ)上，給出一種Web服務(wù)組合Petri網(wǎng)模型的合理性驗證規(guī)則，采用多項式方法，分析網(wǎng)模型的活性及有界性，避免傳統(tǒng)可達(dá)樹等方法帶來的狀態(tài)空間爆炸等問題，簡化了模型求解的復(fù)雜性。但對于復(fù)雜的Web服務(wù)組合網(wǎng)模型，如何在不破壞原網(wǎng)結(jié)構(gòu)性質(zhì)的基礎(chǔ)上將網(wǎng)調(diào)整為自由選擇網(wǎng)，再利用給出的合理性驗證方法進(jìn)行驗證，還需進(jìn)一步研究。

[參考文獻(xiàn)]

[1]Saleem M Q. A decade of model driven Web services composition frameworks[J].Research Journal of Applied Sciences, Engineering and Technology,2014, 7(20): 4244-4250

[2]Vander A W, VanHee K. Workflow management: models, methods and system[M].The MIT Press, 2002.

[3]吳哲輝.Petri網(wǎng)導(dǎo)論[M].北京:機械工業(yè)出版社,2006.

[4]Cardinale Y, Haddad J E, Manouvrier M ,et al. Web service composition based on Petri nets: review and contribution[M].Springer Berlin Heidelberg, 2013.

[5]Aalst van der W M P. Verification of workflow nets[J].Computer Science, 1997, 48(12): 407-426.

[6]Desel J, Esparza J. Free choice Petri nets[M].Cambridge University Press, 1995.

[7]Kemper P, Bause F. An efficient polynomial-time algorithm to decide liveness and boundedness of free-choice nets[C]// Proceedings of the 13th International Conference on Application and Theory of Petri Nets. Springer-Verlag, 1992:263-278.

[8]陳翔,夏國平,李濤.基于Petri 網(wǎng)的工作流模型合理性研究[J].北京理工大學(xué)學(xué)報, 2004,24(12):1074-1078.

[9]馬炳先,相東明,張正明. Web 服務(wù)組合的Petri 網(wǎng)自動生成方法[J].小型微型計算機系統(tǒng),2013,34(2):332-337.

[10]劉士喜,胡曉靜.BPEL到PNML文件轉(zhuǎn)換框架的設(shè)計與實現(xiàn)[J].計算機應(yīng)用與軟件,2013,30(5):60-64.

[11]張金泉,倪麗,蔣昌俊,等.Petri 網(wǎng)極小虹吸的計算方法與性能分析[J].計算機學(xué)報,2010,33(3):576-602.

A Rationality Verification Approach for Web Services Composition Model

Hu Xiaojing, Liu Shixi, Wang Tao

(SchoolofComputerandInformationEngineering,ChuzhouUniversity,Chuzhou,Anhui239000,China)

Key Words：Web service; Petri net; rationality verification; free choice net

(責(zé)任編輯：張凱兵)