基于Petri網自動化構建BPEL流程的SMV模型?

周子健 劉冬梅

（南京理工大學計算機學院 南京 210094）

1 引言

Web服務是當今流行的面向服務架構的基礎，Web服務的廣泛應用使得分布式系統更為靈活。而隨著互聯網技術的急速發展，單一的Web服務早已不能滿足用戶的需求，Web服務組合技術能將已有的功能單一的服務聚合起來構建功能更強大的服務，因此得以迅速發展。WS-BPEL（Web Service Business Process Execution Language）［1］是一種為研究機構和企業所廣泛使用的Web服務組合標準。在組合Web服務的過程中，當開發者所組合的Web服務數量過多時，其組合過程的設計也會隨之變得復雜，在服務組合的設計中，語法的檢查能由編輯器自動完成，但是設計中存在的邏輯問題（比如死鎖、不可達等問題）編輯器卻無法發現，這些問題在設計階段不易檢查出來，在運行時可能會造成巨大的損失，因此需要對BPEL所組合Web服務的正確性進行驗證。

2 自動化構建SMV模型流程

2.1 整體流程

本文提出了一種基于Petri網自動化構建BPEL流程的SMV模型的方法，流程的整體步驟如圖1所示，其主要步驟包括兩個部分。

圖1 自動化構建SMV模型的整體流程

1）BPEL映射到Petri網：將從BPEL代碼中生成Petri網模型，此步驟需先解析BPEL文件，對BPEL的樹形結構進行深度遍歷，過濾其中的非活動節點（如節點、節點等），得到不含活動節點的樹形結構，對活動節點按照不同映射規則映射到Petri網中，再連接各個節點對應的Petri網結構得到BPEL的Petri網模型。

2）Petri網可達圖提取SMV模型：解析所得的Petri網模型，將Petri網的所有庫所的狀態當成一個整體狀態，每次變遷發生Petri網進入下一個狀態，依據此邏輯提取Petri網的可達圖，并依據狀態遷移的過程構建SMV模型。

2.2 BPEL到Petri網結構的映射規則

為從BPEL中生成對應的Petri網結構，需要建立BPEL活動到Petri網結構的映射規則，使用庫所、變遷、有向弧及令牌來地描述BPEL中的活動。

2.2.1 統一映射結構

BPEL中的活動主要分為基本活動和結構化活動兩類，基本活動中包括調用伙伴服務的、與伙伴服務交互時接收消息數據的、向之前接收的請求發送響應的、進行變量更新的、發出內部故障信號的、表示無動作活動的、延遲一段時間或直到達到某個截止時間的，結構化活動中包含控制各個活動之間的順序活動、、和，控制活動之間的并發和同步的，提供由事件控制的活動選擇的等，基本活動與結構化活動組合起來可以表示更為復雜的活動?；净顒映?wait>都是原子活動，內部不含執行的邏輯，及結構化活動內部隱含執行邏輯，映射到Petri網需要對其進行擴展。

BPEL活動的統一表示如圖2（a）所示，Act表示一個完整的活動，一個完整的活動包含P1、P2兩個庫所和一個變遷T，P1、P2分別表示一個活動的初始狀態和活動的結束狀態，T表示一個活動的執行。在執行過程中，前一活動的結束狀態作為后一活動的執行的初始狀態?；净顒优c結構化活動的差異在于基本活動（除外）中變遷表示一個原子活動的執行，而結構化活動中，變遷T可以表示另一個結構化活動，結構化活動中可以包含其他子活動。圖2（b）表示一個活動的隱含的Skip動作，活動可能會由于某種原因不執行，如發生錯誤或者事件等情況，需要終止并跳過該活動，當出現該情況時skip變遷發生表示該活動的跳過。結構化活動跳過的情況在映射中表現為構成結構化活動的內部所有基本活動均發生skip變遷（為簡化說明，后文中如不涉及活動的跳過，均以圖2（a）的表現形式表示代替圖2（b））。

圖2 BPEL活動的統一Petri網結構

2.2.2 含執行邏輯的活動的映射

在基本活動中，較為特殊，其中隱含一定的執行邏輯，故在圖3中對其映射進行說明。含執行邏輯的活動的BPEL代碼與映射到petri網中的模型如圖3所示，所有結構化的活動均有且僅有一個初始庫所表示其執行活動前的狀態，一個結束庫所表示執行完該活動之后的狀態。

圖3 帶執行邏輯的活動的BPEL到Petri網的映射

2.2.3 Scope

是一種特殊的活動，在BPEL規范2.0中并未將其作為基本活動或者結構化活動而是單獨列出介紹。僅用于標識變量、合作伙伴鏈接、消息交換、關聯集、事件處理程序、錯誤處理程序等事件的作用域。下面主要介紹兩個常用的中的活動：錯誤處理程序與事件處理程序對應的Petri網結構。

在BPEL中，用來處理活動所產生的異常，活動必須包含在活動中。當活動A執行過程中出現特定類型的錯誤時，會捕獲到指定類型的錯誤并基于預定義的活動對錯誤進行處理。

為簡化說明，圖4中只列舉了一個活動的情況且隱藏了skip變遷，當BPEL代碼中存在多個分支時，只需加入多個FH分支即可。在BPEL中，事件處理活動用于處理發生的特定事件，包括WSDL操作的返回消息和警告事件，由于的處理邏輯映射到Petri網結構與類似，故不再贅述。

圖4 與活動到Petri網的映射

當一個活動中既包含又包含時，其映射到Petri網中的結構如圖5所示，因與的主體活動相同，錯誤處理分支與事件處理分支需要同時開始等待主體活動A拋出錯誤信息或者對應的事件處理信息。當活動A發生錯誤拋出錯誤信息時，會執行錯誤處理分支并停止事件處理分支，映射到Petri網中表現為get變遷缺少主體活動A傳來的事件消息而始終無法發生，最終事件處理分支上的token會在錯誤處理結束后傳到錯誤處理分支以正常結束活動。若無錯誤發生也無對應的消息事件產生，兩條分支上的token會傳回主體活動路線以正常結束流程，確保對應的Petri網中無多余token遺留。

圖5 包含錯誤處理與事件處理的scope活動到Petri網的映射

至此，本文已將絕大多數BPEL的活動到Petri網結構之間建立了映射，由該映射規則建立的Petri網結構能有效表達其活動執行的邏輯順序，并總能保證當給初始庫所傳入一個token時，執行完成后整個活動對應的Petri網結構中只有結束庫所中有且僅有一個token。

2.3 Petri網到SMV模型的映射規則

SMV的有限狀態模型（FSM）包括定義一個模塊、聲明狀態變量、定義初始狀態和狀態遷移、定義不確定性規則等幾個部分。SMV形式化模型使用MODULE關鍵字定義模塊；使用關鍵字VAR聲明模型的狀態變量；使用關鍵字ASSIGN定義系統的初始狀態和狀態之間的遷移關系；用集合形式的表達式給出該變量的取值范圍，其變量的定義隨取值范圍存在一定的差別，具體將在3.2小節的算法中體現。表1中說明可達圖中元素到SMV的語法之間的映射。

表1 可達圖中的元素到SMV模型的映射規則

3 實現算法

自動化構建BPEL流程的SMV模型主要包括兩個部分，將從BPEL中按上文的映射規則自動化生成Petri網結構和由Petri網的可達圖生成SMV模型。

3.1 生成Petri網結構

生成Petri網結構的實現主要分為如下三步。

1）解析BPEL文件，返回特定的圖結構，圖中節點對應BPEL中的活動；

2）從圖結構的初始節點其深度優先遍歷整個圖結構，對每個活動都按照映射規則生成Petri網結構，將各個Petri網結構相連接，返回所連接的Petri網結構；

3）根據所返回的Petri網結構生成Petri網。

實現的主要邏輯在∏Traνerse()中，算法的實現如Algorithm1所示。

在該算法中，通過深度優先遍歷樹中的節點，根據節點名稱遞歸地對節點按照映射規則建立對應的Petri網結構，將所得Petri網結構與主體Petri網結構相連接，最終得到完整Petri網。

3.2 生成SMV模型

Petri網到SMV模型的轉化過程的實現首先要使用Petri網工具讀取生成的Petri網文件，并生成可達圖，再由本節中的算法PN2SMV從可達圖自動地生成SMV模型。

在該算法中，根據Petri網的可達圖文件獲取所有庫所的可能變遷以及所有狀態下的token數，對每一種狀態按照可達圖中元素到SMV的語法之間的映射規則寫入SMV文件即可得到最終的SMV模型，算法的實現如Algorithm 2所示。

4 案例研究

本文使用BPEL組合天氣查詢Web服務和飛機航班信息查詢Web服務作為驗證實例。組合這兩個Web服務之后的服務的功能為用戶輸入欲查詢航班的出發城市、到達城市和出發日期，該服務將返回用戶到達城市在到達日期的天氣狀況，以提醒用戶更改出行計劃或做好應對相應天氣的準備。其BPEL活動的整體流程如圖6所示，首先接收用戶的輸入，分配用戶的輸入到對應的變量中，然后調用查詢航班信息的Web服務中的get-Domestic City操作，接收獲得所支持的城市列表，再判斷輸入的城市是否支持，不支持則將錯誤信息分配到指定變量用于返回給用戶，支持則并發調用兩個Web服務查詢相應的天氣和航班信息，同時這兩步操作中可能由于存在時間輸入錯誤（自定義的fault）而獲得特定返回信息，需要進行錯誤處理。此案例中包含、、等8種活動類型。

圖6 案例的整體流程

完成BPEL的編寫之后，使用本文實現的工具從BPEL文件中生成Petri網，其中包含28個庫所，40個變遷，經Tina檢查此petri網是有界的，任一遷移都是初始狀態潛在可引發的。使用Tina獲得該Petri網的可達圖，經由本文的工具生成SMV模型，該模型包含73種狀態，使用NuSMV對該模型的性質進行檢查。屬性及對應的CTL表達式以及輸入NuSMV之后驗證的結果如圖7所示，所有屬性均通過驗證。以上實驗結果表明本文的工作能夠很好地從BPEL的活動流程自動化提取Petri網模型，并由Petri網的可達圖自動化生成SMV模型供用戶檢驗活動流程的屬性，通過該流程與工具能起到減輕人工操作的繁瑣、節省BPEL正確性驗證所需的時間與減少人工建?？赡墚a生的差錯等作用。

圖7 案例的屬性驗證結果

5 相關工作

目前學術界研究自動化建模與驗證BPEL主要從兩個方面著手，一是直接使用自動機描述BPEL的相關性質，并使用模型檢測工具加以驗證，如R.Nakashiro等［2］構建BPEL到Spin所對應的輸入語言Promela的映射，直接從BPEL自動化生成PROME?LA再 驗 證，Xiang Fu等［3］以 及Zhao Wei等［4］從BPEL中提取自動機再自動化轉為PROMELA使用Spin驗證，該部分研究大多只涉及了BPEL中的基本活動和結構化活動，未能將Scope中的幾個特殊活動（錯誤處理，異常處理等）加以驗證，且部分基于自動機驗證的方法將每個活動作為一個狀態，難以表示活動的并發過程，未能完全覆蓋BPEL活動的整體流程；二是將BPEL映射到Petri網，基于Pe?tri網驗證BPEL的部分性質，Parimala N等［5～7］分別使用Petri網、層次Petri網和著色Petri網映射BPEL的規范，對BPEL進行特定屬性的檢查?；赑etri網的驗證方法僅驗證了部分屬性（如有界性、死鎖等），其驗證能力弱于支持LTL或者CTL表達式的模型檢測。

在保證BPEL設計過程的正確性方面的研究，多數使用模型檢測工具進行驗證，如Honghua Cao等［11］提出一種方法，他們先使用UML對BPEL進行可視化地建模，隨后提出了一個將UML活動圖的子集自動轉換為PROMELA的框架，使用模型檢測工具Spin對BPEL的正確性進行驗證，該方法中未能考慮到中的活動。Shin Nakajima［2］同樣使用Spin來驗證BPEL中的行為規范。而Petri網是一種用圖來描述系統元素的異步并發操作的模型，適合描述并發、沖突、同步、資源爭用等系統特性，也是用于驗證服務組合部分特性的常用工具之一。Niels Lohmann［12］提出了一種映射方法，將BPEL 2.0規范映射到了對象Petri網中，并著重介紹了2.0中最新的特性的映射。W.M.P.van der Aalst等［13］的方法與W.M.P.van der Aalst的方法類似，同樣是用對象Petri網映射BPEL的規范，最終將Petri網轉為WF-net，對BPEL進行一致性檢查，并在ProM框架中進行了實現。祝義等［14］則另辟蹊徑建立BPEL到函數式語言CSPM的映射，使用FDR來驗證CSPM所描述的系統。

對于W.M.P.van der Aalst等的工作［13］，使用所實現的工具對文中附錄A.3的BPEL源碼（Execut?able BPEL，整理格式化后840行）進行了轉換，所得到的Petri網模型包含42個庫所和57個變遷，少于文中化簡前的97個庫所90個變遷，多于文中化簡后的26個庫所，27個變遷，但是文中給出的Petri網省略了scope中的庫所與變遷以及所有跳過活動與變遷，實際的Petri網遠比本文工具所得Petri網模型要復雜。

本文從BPEL所組合的服務中自動化地生成對應的Petri網模型，在Petri網中檢查死鎖等可能存在的問題，再由Petri網的可達圖自動化地生成SMV模型，使用模型檢測工具NuSMV檢查模型的安全性和行為屬性，并實現了一個可行的工具，通過案例說明該工具的有效性。

6 結語

本文提出了一種基于Petri網自動化構建BPEL流程的SMV模型的方法，通過將BPEL活動自動化映射到Petri網，并由Petri網可達圖自動化生成SMV模型，實現了驗證過程的自動化，有效地解決了人工驗證的繁瑣與易出錯的情況，保證了驗證過程的準確性，提高了驗證的效率。本文對Scope中的補償處理尚未進行映射，未來將思考其映射方式。本文中Petri網的可達圖還需借助Tina獲得，自動化過程還需一定的手動操作，未來的工作是在所實現的工具中加入可達圖生成功能，使得整個流程更為連貫。本文也還未對生成的Petri網進一步的化簡以減少SMV模型中狀態的數量，未來將在一定程度上化簡Petri網，減輕狀態爆炸的問題。