周子健 劉冬梅

（南京理工大學(xué)計算機學(xué)院 南京 210094）

1 引言

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

2 自動化構(gòu)建SMV模型流程

2.1 整體流程

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

圖1 自動化構(gòu)建SMV模型的整體流程

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

2）Petri網(wǎng)可達圖提取SMV模型：解析所得的Petri網(wǎng)模型，將Petri網(wǎng)的所有庫所的狀態(tài)當(dāng)成一個整體狀態(tài)，每次變遷發(fā)生Petri網(wǎng)進入下一個狀態(tài)，依據(jù)此邏輯提取Petri網(wǎng)的可達圖，并依據(jù)狀態(tài)遷移的過程構(gòu)建SMV模型。

2.2 BPEL到Petri網(wǎng)結(jié)構(gòu)的映射規(guī)則

為從BPEL中生成對應(yīng)的Petri網(wǎng)結(jié)構(gòu)，需要建立BPEL活動到Petri網(wǎng)結(jié)構(gòu)的映射規(guī)則，使用庫所、變遷、有向弧及令牌來地描述BPEL中的活動。

2.2.1 統(tǒng)一映射結(jié)構(gòu)

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

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

圖2 BPEL活動的統(tǒng)一Petri網(wǎng)結(jié)構(gòu)

2.2.2 含執(zhí)行邏輯的活動的映射

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

圖3 帶執(zhí)行邏輯的活動的BPEL到Petri網(wǎng)的映射

2.2.3 Scope

是一種特殊的活動，在BPEL規(guī)范2.0中并未將其作為基本活動或者結(jié)構(gòu)化活動而是單獨列出介紹。僅用于標(biāo)識變量、合作伙伴鏈接、消息交換、關(guān)聯(lián)集、事件處理程序、錯誤處理程序等事件的作用域。下面主要介紹兩個常用的中的活動：錯誤處理程序與事件處理程序?qū)?yīng)的Petri網(wǎng)結(jié)構(gòu)。

在BPEL中，用來處理活動所產(chǎn)生的異常，活動必須包含在活動中。當(dāng)活動A執(zhí)行過程中出現(xiàn)特定類型的錯誤時，會捕獲到指定類型的錯誤并基于預(yù)定義的活動對錯誤進行處理。

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

圖4 與活動到Petri網(wǎng)的映射

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

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

至此，本文已將絕大多數(shù)BPEL的活動到Petri網(wǎng)結(jié)構(gòu)之間建立了映射，由該映射規(guī)則建立的Petri網(wǎng)結(jié)構(gòu)能有效表達其活動執(zhí)行的邏輯順序，并總能保證當(dāng)給初始庫所傳入一個token時，執(zhí)行完成后整個活動對應(yīng)的Petri網(wǎng)結(jié)構(gòu)中只有結(jié)束庫所中有且僅有一個token。

2.3 Petri網(wǎng)到SMV模型的映射規(guī)則

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

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

3 實現(xiàn)算法

自動化構(gòu)建BPEL流程的SMV模型主要包括兩個部分，將從BPEL中按上文的映射規(guī)則自動化生成Petri網(wǎng)結(jié)構(gòu)和由Petri網(wǎng)的可達圖生成SMV模型。

3.1 生成Petri網(wǎng)結(jié)構(gòu)

生成Petri網(wǎng)結(jié)構(gòu)的實現(xiàn)主要分為如下三步。

1）解析BPEL文件，返回特定的圖結(jié)構(gòu)，圖中節(jié)點對應(yīng)BPEL中的活動；

2）從圖結(jié)構(gòu)的初始節(jié)點其深度優(yōu)先遍歷整個圖結(jié)構(gòu)，對每個活動都按照映射規(guī)則生成Petri網(wǎng)結(jié)構(gòu)，將各個Petri網(wǎng)結(jié)構(gòu)相連接，返回所連接的Petri網(wǎng)結(jié)構(gòu)；

3）根據(jù)所返回的Petri網(wǎng)結(jié)構(gòu)生成Petri網(wǎng)。

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

在該算法中，通過深度優(yōu)先遍歷樹中的節(jié)點，根據(jù)節(jié)點名稱遞歸地對節(jié)點按照映射規(guī)則建立對應(yīng)的Petri網(wǎng)結(jié)構(gòu)，將所得Petri網(wǎng)結(jié)構(gòu)與主體Petri網(wǎng)結(jié)構(gòu)相連接，最終得到完整Petri網(wǎng)。

3.2 生成SMV模型

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

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

4 案例研究

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

圖6 案例的整體流程

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

圖7 案例的屬性驗證結(jié)果

5 相關(guān)工作

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

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

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

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

6 結(jié)語

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