陳瑩1，邢建春1，王洪達(dá)1，楊啟亮1,2

　?。?.解放軍理工大學(xué) 國(guó)防工程學(xué)院，江蘇 南京 210007；2.南京大學(xué) 計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室，江蘇 南京 210093）

      摘要：針對(duì)BPEL過(guò)程在死路徑消除語(yǔ)義下建模與分析不夠完善的問(wèn)題，提出了一種新的BPEL過(guò)程建模與分析方法。該方法建立了將BPEL死路徑消除語(yǔ)義轉(zhuǎn)化為普通if-then-else的規(guī)則，進(jìn)而可以利用著色Petri網(wǎng)（CPN）形式化地對(duì)BPEL過(guò)程進(jìn)行建模，并通過(guò)CPNTools對(duì)BPEL過(guò)程的建模進(jìn)行自動(dòng)分析及驗(yàn)證。案例分析表明，該方法具有一定的實(shí)用性和可行性，能夠幫助軟件工程人員更好地測(cè)試、調(diào)試和維護(hù)BPEL程序。

　　關(guān)鍵詞：Web服務(wù)組合；BPEL程序依賴(lài)圖；死路徑語(yǔ)義消除；著色Petri網(wǎng)

　　中圖分類(lèi)號(hào)：TP311.5文獻(xiàn)標(biāo)識(shí)碼：ADOI： 10.19358/j.issn.1674-7720.2017.06.008

　　引用格式：陳瑩，邢建春，王洪達(dá)，等. 死路徑消除語(yǔ)義下的BPEL過(guò)程建模與分析［J］.微型機(jī)與應(yīng)用，2017,36（6）：22-25.

0引言

　　*基金項(xiàng)目：江蘇省自然科學(xué)基金項(xiàng)目（BK20151451）Web服務(wù)業(yè)務(wù)過(guò)程執(zhí)行語(yǔ)言（BPEL或者WSBPEL）是為滿(mǎn)足基于服務(wù)的業(yè)務(wù)流程需要而制定的業(yè)界事實(shí)標(biāo)準(zhǔn)［1］。基于BPEL的組合Web服務(wù)因其能夠提供功能更加強(qiáng)大的服務(wù)而受到業(yè)界的廣泛認(rèn)可［2］。然而，服務(wù)業(yè)務(wù)流程并不總是完美的，在流程設(shè)計(jì)中往往會(huì)存在一些問(wèn)題（比如死路徑消除），這很難滿(mǎn)足高可靠度和可行性的要求。因此，BPEL過(guò)程在死路徑消除語(yǔ)義下建模與分析的問(wèn)題仍然需要完善。所謂死路徑消除是指擴(kuò)大某個(gè)不可執(zhí)行活動(dòng)的范圍以至在該活動(dòng)執(zhí)行完成之后執(zhí)行的所有活動(dòng)都將無(wú)法完成。每個(gè)活動(dòng)都承載著充當(dāng)下一個(gè)活動(dòng)是否能執(zhí)行的判定條件的角色。目前，有關(guān)BPEL過(guò)程建模分析與驗(yàn)證的技術(shù)主要有Petri網(wǎng)［3］、進(jìn)程代數(shù)［4］和自動(dòng)機(jī)［5］等方法。從BREUGL F V［6］分析的近100篇論文中發(fā)現(xiàn)，采用進(jìn)程代數(shù)和自動(dòng)機(jī)的方法對(duì)BPEL過(guò)程進(jìn)行建模，其模型比較復(fù)雜抽象，建模過(guò)程難度比較大。又由于BPEL程序同時(shí)支持并發(fā)路徑和死路徑消除（Dead Path Elimination, DPE），為了最大程度地解決BPEL過(guò)程建模的并發(fā)路徑和死路徑消除問(wèn)題，需對(duì)現(xiàn)有的傳統(tǒng)建模方法進(jìn)行改進(jìn)。

　　基于業(yè)務(wù)流程的復(fù)雜性，使用BPEL流程組合建模比較容易出現(xiàn)錯(cuò)誤［7］，并且在語(yǔ)言表達(dá)上不夠簡(jiǎn)明易懂。為了使流程語(yǔ)言表達(dá)更加準(zhǔn)確、簡(jiǎn)單，需要采用形式化的方法對(duì)BPEL過(guò)程進(jìn)行建模與分析。

　　本文基于著色Petri網(wǎng)對(duì)BPEL過(guò)程在死路徑消除語(yǔ)義下進(jìn)行建模。著色Petri網(wǎng)（Colored Petri Net, CPN）是對(duì)一般Petri網(wǎng)的擴(kuò)展，具有Petri網(wǎng)的所有性質(zhì)，它將Petri網(wǎng)與程序元語(yǔ)言（Meta Language，ML）結(jié)合，并以簡(jiǎn)潔明了的方式描述并發(fā)系統(tǒng)。本文的主要?jiǎng)?chuàng)新點(diǎn)是在已有工作的基礎(chǔ)上，提出了一種死路徑消除語(yǔ)義下的BPEL過(guò)程建模與分析方法，該方法建立了將BPEL死路徑消除語(yǔ)義轉(zhuǎn)化為普通ifthenelse的規(guī)則，并采用CPNTools工具將其形式化地表現(xiàn)出來(lái)。通過(guò)案例分析表明，與現(xiàn)有的BPEL過(guò)程建模相比，本文提出的BPEL過(guò)程在死路徑消除語(yǔ)義下的建模更具有實(shí)用性和可行性，從而能夠幫助軟件工程師更好地測(cè)試、調(diào)試和維護(hù)BPEL程序。

1相關(guān)概念

　　1.1BPEL簡(jiǎn)介與死路徑消除

　　BPEL是一種使用XML（標(biāo)準(zhǔn)通用標(biāo)記語(yǔ)言下的一個(gè)子集）編寫(xiě)的服務(wù)組合編制語(yǔ)言，用于自動(dòng)化業(yè)務(wù)流程的形式規(guī)約語(yǔ)言，可以協(xié)調(diào)多個(gè)服務(wù)的執(zhí)行。由于業(yè)務(wù)流程的需要，BPEL提供了基本活動(dòng)與結(jié)構(gòu)化活動(dòng)兩種不同的活動(dòng)類(lèi)型［8］。同時(shí)，BPEL使用<flow>來(lái)提供并發(fā)性，并發(fā)活動(dòng)的同步用<link>表示。

　　一個(gè)BPEL活動(dòng)可以是多個(gè)<link>的源活動(dòng)，這些<link>稱(chēng)為該活動(dòng)的outgoing links［9］?；顒?dòng)結(jié)束時(shí)，根據(jù)每個(gè)<link>對(duì)應(yīng)的變遷條件對(duì)<link>狀態(tài)進(jìn)行設(shè)置（true or false）。如果沒(méi)有與明確的變遷條件相關(guān)聯(lián)，則默認(rèn)的變遷條件為真。一個(gè)活動(dòng)同時(shí)也可以是多個(gè)<link>的目標(biāo)活動(dòng)，這些<link>稱(chēng)為該活動(dòng)的incoming links。關(guān)于incoming links狀態(tài)的變量構(gòu)成的布爾表達(dá)式，定義為BPEL過(guò)程融合條件（join condition）。只有當(dāng)融合條件為真時(shí)，活動(dòng)才可以執(zhí)行。當(dāng)所有的<link>取得了某種狀態(tài)后，這個(gè)連接條件的值才能確定下來(lái)［10］。如果這個(gè)連接條件是真，則活動(dòng)可以被執(zhí)行，反之如果連接條件為假，則該活動(dòng)不能執(zhí)行并且所有通過(guò)它的<link>均被置為假。這樣的狀態(tài)將一直向下傳遞直到遇到某個(gè)活動(dòng)的變遷條件為真，此時(shí)目標(biāo)活動(dòng)才可以執(zhí)行，這種技術(shù)稱(chēng)之為死路徑消除。

　　1.2CPN簡(jiǎn)介

　　著色Petri網(wǎng)（Colored Petri Net, CPN）是由丹麥研究員Kurt Jensen于1981年所提出，與大家所熟知的基本Petri網(wǎng)一樣，CPN也是由庫(kù)所、變遷和弧所組成［11］，但不同的是CPN加入了元素聲明并且具有對(duì)系統(tǒng)進(jìn)行仿真和驗(yàn)證的能力。CPN結(jié)合了基本Petri網(wǎng)和程序語(yǔ)言的優(yōu)點(diǎn)，可將復(fù)雜的業(yè)務(wù)流程用圖形的方式進(jìn)行建模描述，使得流程變得簡(jiǎn)單、更易于理解。此外，還可以運(yùn)用一種強(qiáng)大的著色Petri網(wǎng)仿真工具CPNTools對(duì)系統(tǒng)的有界性、活性及其公平性等性質(zhì)進(jìn)行驗(yàn)證。本文的案例就是運(yùn)用了此工具進(jìn)行仿真、驗(yàn)證和分析，從而證實(shí)了文中所提出規(guī)則的準(zhǔn)確性。

　　定義［9］：一個(gè)CPN是由一個(gè)九元組 CPN=(∑, P,T,A,N,C,G,E,I)所組成的。式中：

　　∑表示顏色（Color）的非空有限集合；

　　P：描述系統(tǒng)庫(kù)所（Place）的有限集合；

　　T：變遷（Transition）的有限集合；

　　A：?。ˋrc）的有限集合，滿(mǎn)足P∩T=P∩A=A∩T=；

　　N：A→（P×T∪T×P）為節(jié)點(diǎn)（Node）函數(shù)；

　　C：（P∪T）→∑ss為顏色函數(shù)，其中∑ss為∑的有限子集；

　　G：T→表達(dá)式為T(mén)的守衛(wèi)函數(shù)，即∨t∈T，［Type(G(t))=B∧Type(Var(G(t)))∑］，其中Type(v)表示變量v的類(lèi)型，Var（exp r）表示表達(dá)式exp r中的變量集合；

　　E：A→表達(dá)式是弧表達(dá)式函數(shù)，形如∨a∈A，［Type(E(a))=C(P(a))ms∧Type(Var(E(a)))∑］;

　　I：P→表達(dá)式的初始標(biāo)示，形如∨p∈P，［Type(I(p))=C(P)ms］。

　　2DPE語(yǔ)義下的BPEL過(guò)程建模中的轉(zhuǎn)換規(guī)則

　　關(guān)于BEPL到Petri網(wǎng)的映射規(guī)則，早在2004年德國(guó)柏林Humboldt University的HINZ S等提出了一套完整的BPEL到Petri網(wǎng)轉(zhuǎn)化規(guī)則［12］。而且STAHL C還在他的碩士畢業(yè)論文中提到了死路徑消除語(yǔ)義下的建模規(guī)則，為消除死路徑模型，他們建立了一個(gè)鏈接模式，嵌入一個(gè)活動(dòng)［12］。而本文的貢獻(xiàn)主要是提出一種將BPEL死路徑消除語(yǔ)義轉(zhuǎn)化為普通ifthenelse的規(guī)則，并將其形式化的表述出來(lái)。

　　在BPEL中，將<link>活動(dòng)看作一項(xiàng)基本活動(dòng)，把它的連接條件看作是這個(gè)活動(dòng)的決定性條件。根據(jù)<link>活動(dòng)和DPE語(yǔ)義，有如下四條規(guī)則可以覆蓋所有的情況。

　　其中定義3個(gè)顏色集：

　　colset E=with e; colset L=bool;

　　colset ACTIVE=product L×E;

　　9個(gè)變量：

　　var l，lA，lB，l1，l2，l3，jc，ran：L，a：E。

　　2個(gè)函數(shù)：

　　fun OK (l1：L) = (l1 = true)；

　　fun Skip(l1：L) = (l1 = false)。

　　規(guī)則 1：?jiǎn)芜B接。如圖1所示，Activity A、Activity B、Activity C分別表示三個(gè)基本活動(dòng)，而且這三個(gè)活動(dòng)都在活動(dòng)<flow>中。箭頭線(xiàn)表示兩個(gè)活動(dòng)之間的控制流，加粗線(xiàn)表示<link>活動(dòng)。Activity B的變遷條件是tc1，Activity B的連接條件是一個(gè)默認(rèn)值為真。根據(jù)DPE語(yǔ)義，單<link>連接的轉(zhuǎn)換規(guī)則可以用圖2來(lái)說(shuō)明。在這個(gè)轉(zhuǎn)換中，將<link>轉(zhuǎn)化為正常的控制流結(jié)點(diǎn)并且活動(dòng)表示為l1=tc1。因此可用傳統(tǒng)的分析方法來(lái)分析BPEL程序的路徑可行性。

　　圖1中的活動(dòng)網(wǎng)中，庫(kù)所Start Activity A表示活動(dòng)A的初始狀態(tài)，其顏色集為ACTIVE。當(dāng)托肯值是(true，e)時(shí)，表示活動(dòng)A能正常運(yùn)行，根據(jù)弧表達(dá)式的運(yùn)算，觸發(fā)變遷Activity B，使得其中一個(gè)case語(yǔ)句被執(zhí)行，其他語(yǔ)句被跳過(guò)，表示活動(dòng)B正常運(yùn)行［9］。另一方面，當(dāng)托肯值為（false，e）時(shí)，則會(huì)觸發(fā)變遷Skipping B，表示活動(dòng)B被跳過(guò)。庫(kù)所Finish Activity C的托肯值表示活動(dòng)最終的狀態(tài)，即活動(dòng)是否正常執(zhí)行。

　　規(guī)則2：兩個(gè)相連的<link>。如有兩個(gè)<link>相繼連接，可用圖2來(lái)表示轉(zhuǎn)換規(guī)則。

　　規(guī)則 3：一個(gè)<link>有兩個(gè)后繼<link>。如果一個(gè)<link>后面有兩個(gè)后繼<link>，則轉(zhuǎn)換規(guī)則如圖3所示。

　　規(guī)則4：一個(gè)<link>的源活動(dòng)中包含一個(gè)謂詞活動(dòng)（<while>，<if>，<pick>）。如果一個(gè)<link>的源活動(dòng)中包含一個(gè)斷言式結(jié)構(gòu)，則轉(zhuǎn)換規(guī)則如圖4所示。圖中，活動(dòng)F的執(zhí)行與否取決于謂詞活動(dòng)（例如<if>），因此，活動(dòng)l1表示l1=if(if表示謂詞活動(dòng)的決定條件)。

　　由于規(guī)則2至規(guī)則4活動(dòng)網(wǎng)的運(yùn)行規(guī)則與規(guī)則1相似，限于篇幅，此處不再贅述。

　　以上4個(gè)規(guī)則中，每個(gè)目標(biāo)活動(dòng)的<link>是一個(gè)基本活動(dòng)，如果目標(biāo)活動(dòng)是一個(gè)結(jié)構(gòu)活動(dòng)，活動(dòng)包括它本身也將被忽略。同時(shí)將一直應(yīng)用這4個(gè)規(guī)則，直到BPEL程序中不再有這種結(jié)構(gòu)。

3案例分析

　　3.1案例描述

　　在本節(jié)中，采用了WSBPEL 2.0Primer［1］的例子來(lái)評(píng)估此方法。在圖5的示例中，四個(gè)活動(dòng)是并發(fā)執(zhí)行的。<flow>活動(dòng)開(kāi)始時(shí)，四個(gè)活動(dòng)同時(shí)開(kāi)始執(zhí)行。由于<link>的變遷條件是完全相反的（大于或等于5 000），這意味著兩個(gè)后繼活動(dòng)approve Credit或decline Credit中只有一個(gè)將被執(zhí)行。

　　在設(shè)計(jì)BPEL控制流圖時(shí)，當(dāng)沒(méi)有考慮DPE的控制流圖的情況時(shí)，有些死鎖等問(wèn)題是檢測(cè)不出來(lái)的。而當(dāng)考慮了DPE后，這些死鎖問(wèn)題就可以被檢測(cè)出來(lái)。因此，死路徑消除語(yǔ)義下的BPEL過(guò)程建模與分析是很有必要的。

　　3.2建模與分析

　　根據(jù)BPEL流程的CPN映射規(guī)則進(jìn)行建模，整個(gè)案例是由兩個(gè)flow活動(dòng)、一個(gè)switch活動(dòng)和High Risk、Low Risk、Reply以及Invoke四個(gè)基本活動(dòng)所組成。其中，flow活動(dòng)由庫(kù)所Begin Flow和庫(kù)所End Flow之間的部分所組成，switch活動(dòng)由庫(kù)所Begin Switch和庫(kù)所End Switch之間的部分所組成，限于篇幅，案例圖略。

　　對(duì)于以上案例的CPN模型，運(yùn)用CPNTools的狀態(tài)空間分析工具對(duì)模型的性質(zhì)進(jìn)行自動(dòng)驗(yàn)證，圖6是描述活動(dòng)性質(zhì)的數(shù)據(jù)，從圖中可看出，模型中不存在死標(biāo)識(shí)，也不存在不可發(fā)生的變遷，也就是說(shuō)全部變遷都是活性的，因此整個(gè)案例模型滿(mǎn)足活性性質(zhì)的要求，從而驗(yàn)證了案例的合理性。

4結(jié)束語(yǔ)

　　本文基于BPEL控制流圖（考慮了并發(fā)結(jié)構(gòu)和DPE語(yǔ)圖4包含謂詞活動(dòng)的轉(zhuǎn)換示意圖圖5一個(gè)典型的程序義），提出了一種新的分析BPEL過(guò)程路徑可行性方法，主要貢獻(xiàn)分為兩個(gè)方面。第一，一個(gè)新型的BPEL控制流圖，即一個(gè)控制流圖能抽象出WSBPEL程序的執(zhí)行過(guò)程并考慮了死路徑消除語(yǔ)義。第二，應(yīng)用CPNTools工具，將復(fù)雜的BPEL控制流圖轉(zhuǎn)換為較簡(jiǎn)單明了的流圖，并運(yùn)用CPN中狀態(tài)空間分析工具對(duì)其進(jìn)行有界性、活性等分析，從而驗(yàn)證了方法的可行性。

參考文獻(xiàn)

　　［1］ Wang Hongda, Xing Jianchun, Yang Qiliang,et al. Optimal control based regression test selection for service-oriented workflow applications［J］. Journal of Systems & Software, 2016, 124:274-288.

　?。?］ 鄭劍，江建慧. Web服務(wù)軟件測(cè)試技術(shù)進(jìn)展［J］. 計(jì)算機(jī)應(yīng)用與軟件，2009，26（10）：101-104.

　?。?］ HINZ S，SCHMIDT K，STAHL C. Transforming BPEL to Petri Nets［C］.Proceeding of the 3rd International Conference on Business Process Management (BPM 2005)， Berlin，2005: 220235.［4］ FERRARA A. Web services: a process algebra approach［C］. Proceedings of the 2nd Internationa Couference on Service Oriented Computing. New York: ACM Press, 2004：242-251.

　　［5］ FOSTER H, UCHITEL S, MAGEE J, et al. Modelbased verification of Web service compositions［C］.

　　Proceedings of the 18th IEEE International Conference on Automated Software Engineering, 2003：152-161.

　?。?］ BREUGEL F V, KOSHKINA M. Models and verification of BPEL［EB/OL］.（200609xx）［2016-10-19］http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf. September 2006.

　　［7］ OUYANG C, BREUTAL S. WofBPEL: a tool for automaed analysis of BPEL processes ［J］. Lecture Notes in Computer Science，2005，3826: 484489.

　?。?］ 余港. BPEL中基于異步模式的人工任務(wù)執(zhí)行系統(tǒng)的研究與實(shí)現(xiàn)［D］. 重慶:重慶大學(xué)，2010.

　　［9］ STAHL C. Transformation von BPEL4WS in Petrinetze［D］. Berlin: Humboldt University at zu Berlin, 2004.

　?。?0］ 駱翔宇，王昆，王鳳釵. 一種Web服務(wù)組合的認(rèn)知模型檢測(cè)方法［J］.小型微型計(jì)算機(jī)系統(tǒng)，2011，32(10)：2042-2047.

　?。?1］ 彭潔. 基于著色Petri網(wǎng)的工作流建模與實(shí)現(xiàn)［D］. 南昌：江西理工大學(xué)，2009.

　?。?2］ 門(mén)鵬，段振華. 基于著色Petri網(wǎng)的BPEL建模與驗(yàn)證［J］.西北大學(xué)學(xué)報(bào)，2007，37(6)：986-990.