基于Petri網(wǎng)自動(dòng)化構(gòu)建BPEL流程的SMV模型?

周子健 劉冬梅

（南京理工大學(xué)計(jì)算機(jī)學(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ù)早已不能滿(mǎn)足用戶(hù)的需求，Web服務(wù)組合技術(shù)能將已有的功能單一的服務(wù)聚合起來(lái)構(gòu)建功能更強(qiáng)大的服務(wù)，因此得以迅速發(fā)展。WS-BPEL（Web Service Business Process Execution Language）［1］是一種為研究機(jī)構(gòu)和企業(yè)所廣泛使用的Web服務(wù)組合標(biāo)準(zhǔn)。在組合Web服務(wù)的過(guò)程中，當(dāng)開(kāi)發(fā)者所組合的Web服務(wù)數(shù)量過(guò)多時(shí)，其組合過(guò)程的設(shè)計(jì)也會(huì)隨之變得復(fù)雜，在服務(wù)組合的設(shè)計(jì)中，語(yǔ)法的檢查能由編輯器自動(dòng)完成，但是設(shè)計(jì)中存在的邏輯問(wèn)題（比如死鎖、不可達(dá)等問(wèn)題）編輯器卻無(wú)法發(fā)現(xiàn)，這些問(wèn)題在設(shè)計(jì)階段不易檢查出來(lái)，在運(yùn)行時(shí)可能會(huì)造成巨大的損失，因此需要對(duì)BPEL所組合Web服務(wù)的正確性進(jìn)行驗(yàn)證。

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

2.1 整體流程

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

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

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

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

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

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

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

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

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

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

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

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

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

2.2.3 Scope

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

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

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

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

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

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

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

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

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

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

3 實(shí)現(xiàn)算法

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

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

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

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

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

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

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

在該算法中，通過(guò)深度優(yōu)先遍歷樹(shù)中的節(jié)點(diǎn)，根據(jù)節(jié)點(diǎn)名稱(chēng)遞歸地對(duì)節(jié)點(diǎn)按照映射規(guī)則建立對(duì)應(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)化過(guò)程的實(shí)現(xiàn)首先要使用Petri網(wǎng)工具讀取生成的Petri網(wǎng)文件，并生成可達(dá)圖，再由本節(jié)中的算法PN2SMV從可達(dá)圖自動(dòng)地生成SMV模型。

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

4 案例研究

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

圖6 案例的整體流程

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

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

5 相關(guān)工作

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

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

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

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

6 結(jié)語(yǔ)

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