2017-04-10 16:44:55

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

  (1.解放軍理工大學 國防工程學院,江蘇 南京 210007;2.南京大學 計算機軟件新技術國家重點實驗室,江蘇 南京 210093)

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

  關鍵詞:Web服務組合;BPEL程序依賴圖;死路徑語義消除;著色Petri網

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

  引用格式:陳瑩,邢建春,王洪達,等. 死路徑消除語義下的BPEL過程建模與分析[J].微型機與應用,2017,36(6):22-25.

0引言

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

  基於業務流程的複雜性,使用BPEL流程組合建模比較容易出現錯誤[7],並且在語言表達上不夠簡明易懂。為了使流程語言表達更加準確、簡單,需要采用形式化的方法對BPEL過程進行建模與分析。

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

1相關概念

  1.1BPEL簡介與死路徑消除

  BPEL是一種使用XML(標準通用標記語言下的一個子集)編寫的服務組合編製語言,用於自動化業務流程的形式規約語言,可以協調多個服務的執行。由於業務流程的需要,BPEL提供了基本活動與結構化活動兩種不同的活動類型[8]。同時,BPEL使用<flow>來提供並發性,並發活動的同步用<link>表示。

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

  1.2CPN簡介

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

第1頁  第2頁  第3頁  

http://www.autooo.net/autooo/wuxiantongxun/jishu/2017-04-10/171609.html