陳瑩1，邢建春1，王洪達1，楊啟亮1,2

　?。?.解放軍理工大學 國防工程學院，江蘇 南京 210007；2.南京大學 計算機軟件新技術國家重點實驗室，江蘇 南京 210093）

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

　　關鍵詞：Web服務組合；BPEL程序依賴圖；死路徑語義消除；著色Petri網(wǎng)

　　中圖分類號：TP311.5文獻標識碼：ADOI： 10.19358/j.issn.1674-7720.2017.06.008

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

0引言

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

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

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

1相關概念

　　1.1BPEL簡介與死路徑消除

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

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

　　1.2CPN簡介

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

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

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

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

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

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

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

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

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

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

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

　　2DPE語義下的BPEL過程建模中的轉換規(guī)則

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

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

　　其中定義3個顏色集：

　　colset E=with e; colset L=bool;

　　colset ACTIVE=product L×E;

　　9個變量：

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

　　2個函數(shù)：

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

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

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

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

　　規(guī)則2：兩個相連的<link>。如有兩個<link>相繼連接，可用圖2來表示轉換規(guī)則。

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

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

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

　　以上4個規(guī)則中，每個目標活動的<link>是一個基本活動，如果目標活動是一個結構活動，活動包括它本身也將被忽略。同時將一直應用這4個規(guī)則，直到BPEL程序中不再有這種結構。

3案例分析

　　3.1案例描述

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

　　在設計BPEL控制流圖時，當沒有考慮DPE的控制流圖的情況時，有些死鎖等問題是檢測不出來的。而當考慮了DPE后，這些死鎖問題就可以被檢測出來。因此，死路徑消除語義下的BPEL過程建模與分析是很有必要的。

　　3.2建模與分析

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

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

4結束語

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

參考文獻

　?。?］ 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服務軟件測試技術進展［J］. 計算機應用與軟件，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.

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

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

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

　　［10］ 駱翔宇，王昆，王鳳釵. 一種Web服務組合的認知模型檢測方法［J］.小型微型計算機系統(tǒng)，2011，32(10)：2042-2047.

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

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