基于π演算的BPEL組合服務的形式化描述及驗證

夏紅星

（江蘇靖江教師進修學校，江蘇 泰州214500）

在SOA系統中，通常根據企業的業務需求，利用BPEL技術將各個獨立的Web服務進行組裝[1]。如何判斷組合后的服務能夠滿足企業的需求，如何判斷組合服務不會在運行中出現問題，這是軟件開發人員交付服務前必須考慮的問題。事實上，人工設計或自動構建的服務組合可能存在死鎖、活鎖、狀態不可達等眾多問題，所以必須在部署前進行嚴格的驗證，以及時發現服務組合中存在的問題。

所謂的Web組合服務驗證就是指在實際部署組合服務系統前，通過某些理論或工具檢查該服務組合流程邏輯的合理性、服務間的兼容性，從而及時發現和修正存在的問題，以免日后運行過程中給企業和用戶造成損失。本文的重點是驗證組合服務的內部流程邏輯[2]。

當前主要是通過基于狀態轉換模型的Petri網理論、自動機理論和基于進程代數模型的π演算理論對Web組合服務進行驗證[1]。采用Petri網或者自動機對服務組合進行描述較直觀簡潔，但是當業務流程復雜、牽扯到的子服務眾多且服務間的交互頻繁的時候，往往會引起狀態空間急劇增加，因此導致驗證復雜度劇增。而π演算正是表示這種復雜行為的有效方式，可以清楚表示系統的并發交互行為。π演算采用文本的進程表達式描述系統，表達能力強且形式簡潔，加之π演算中的行為理論非常適合用來描述動態并發的Web服務，因此本文采用π演算理論對服務組合進行建模和驗證。

1 基于π演算的BPEL服務組合建模

1.1 π演算的語法定義

π演算是由MILNER R等人在通信系統演算CCS的基礎上提出來的描述和分析通信拓撲結構動態變化的計算模型。設N為無限名字集，x、y等小寫字母為名字集上的名字；A、B等表示進程；P、Q等表示進程表達式，進程表達式包括以下幾種形式：

0表示空進程；P+Q表示選擇執行P或者Q，只執行其中一個。

(2)并發表達式：P|Q表示并發執行進程P、Q。

(3)前綴表達式 y(x).P、yx.P、 .P：

正前綴y(x).P表示在端口y上輸入名字 x，然后執行進程P。

負前綴yx.P表示在端口y上輸出x后，再執行進程P；

.P稱為啞前綴，表示進程外部不可見的動作，執行完進程后，再執行 P。

(4)循環表達式：！P表示無窮復制進程P。

(5)限制表達式：(x)P表示進程P在通道x上的外部動作被禁止，但是可以進行在通道x上的內部通信。

(6)匹配表達式：[x=y].P表示當條件x=y成立時才執行進程P。

(7)進程標識符：A（x，y，…，z）對每個進程來說，必須有其定義 A（x，y，…，z）∷=P，其中 x，y，…，z表示進程P中的自由名。

至此，將π演算定義如下：

1.2 BPEL描述的Web組合服務的π演算建模

1.2.1 建模算法

為了利用π演算驗證BPEL服務組合，首先要將Web服務的邏輯關系映射為π演算的表達式，形式化描述Web服務組合，這個過程就是建模，算法描述如下：

(1)將BPEL服務組合中的每個Web服務看作一個π演算的進程。如果該服務本身又是一個組合服務那么將其遞歸細分為一系列的子服務，然后將每個子服務看作一個π演算進程。

(2)服務之間的調用關系抽象成π演算進程之間的通道上的消息交互。兩個相關進程之間至少有一條通道，如果兩進程間有多條順序消息，則抽象成在一條通道上傳遞。

(3)根據 Web組合服務業務流程圖，按照下表所示的Web服務元素與π演算的元素對應關系，將業務流程圖轉換成π演算流圖。對應關系如表1所示。

(4)根據上一步驟產生的π演算流圖，寫出建模表達式，將Web服務及其組合用π演算形式化描述出來。

表1 BPEL中Web服務與π演算元素對應關系

1.2.2 建模實例

下面以基于BPEL的信貸服務系統（由客戶、銀行信貸受理服務、客戶信用評估服務、信貸審批服務組成）為例，進行組合服務的π演算建模。

信貸服務系統的流程是：首先客戶向銀行信貸受理部門提出貸款請求，銀行收到客戶的貸款請求后，詢問客戶的具體貸款信息（比如客戶姓名、貸款數額等），客戶將這些信息反饋給銀行信貸部門；銀行信貸部門將客戶貸款信息提交給客戶信用評價部門，要求對該客戶的信用狀況進行評價，然后信用評價部門將評價信息反饋給信貸受理部門；信貸受理部門將客戶申請信息和信用評價信息匯總初審。如果初審不通過，則直接拒絕客戶的借貸活動；如果初審通過，則通知客戶借貸請求已受理；然后將所有信息提交給審批部門，審批部門將審批結果反饋給信貸受理部門；信貸受理部門最后將審批結果反饋給客戶，通知是否可以對客戶發放貸款。具體業務流程如圖1所示。

根據建模算法，將業務流程圖抽象出如下的π演算流圖，如圖2所示。

根據π演算流圖，寫出借貸系統服務的建模表達式如下：

設客戶-Client、信貸受理服務(Client Accepting Service)-CAS、信用評估服務 Credit Evaluation Service-CES、審批服務-Approving Service-AS。

客戶服務Client在X通道上與信貸受理服務通信：

設u={X,ReqLoan,AskDetails,ProvideDetails,RefuseReq,AcceptReq,InformResult}，則：

信貸受理服務CAS在Y 通道上與信用評估服務通信：

設b={X,Y,Z,ReqLoan,AskDetails,ProvideDetails,Refuse-Req,AcceptReq,InformResult,ReqEvaluation,ReplyEvaluation,ReqApprove,ReplyApprove}，則：

信用評估服務CES在通道Y上與信貸服務通信：設 c={Y,ReqEvaluation,ReplyEvaluation}，則：

CES(c)=Y(msg).[msg=ReqEvaluation]Y.CES(c)

審批服務AS在通道Z上與信貸服務通信：

設 a={Z,ReqApprove,ReplyApprove}，則：

整個信貸服務系統LoanService由信貸受理服務(Client Accepting Service)CAS、信用評估服務(Credit Evaluation Service)CES、審批服務（Approving Service）AS 組合而成。{Y、Z}屬于LoanService的內部通道，作為受限名字出現，于是信貸服務系統的定義如下：

2 基于π演算的BPEL組合服務的驗證

2.1 Web服務組合內部邏輯驗證的內容

Web服務組合內部流程邏輯的驗證主要包括流程的可達性驗證、流程的正確完成性驗證、流程的活鎖驗證、死鎖驗證、觀察等價性驗證等，本文只驗證觀察等價性。驗證觀察等價性也就是驗證兩個進程是否是弱互模擬的。弱互模擬的定義：如果進程P、Q的外部行為是一致的，即模擬進程和被模擬進程在外部觀察者看來具備完全相同的行為能力，其中一個進程能執行的動作另一個進程也能模擬，則稱進程P、Q弱互模擬。

2.2 觀察等價性和死鎖的驗證

本文的驗證除了手工推演，還借助了自動化π演算工具MWB。MWB采用基于New Jersey SML語言編譯器，適用于操作和分析動態并發系統。

理論推演：在前面建模時，將Client建模為π演算進程，這樣做是出于下面驗證觀察等價性的需要。根據π演算相關理論和參考文獻[3]提出的反轉證明法，要判斷系統中π演算描述的Client的逆進程ReverseClient與LoanService是否觀察等價，只需要判斷ReverseClient與LoanService是否是弱互模擬的。

Client的逆進程為：

設u={X,ReqLoan,AskDetails,ProvideDetails,RefuseReq,AcceptReq,InformResult}，則：

在組合服務 LoanService中，Y、Z是服務內部的私有通道，在這兩個通道上的動作集{ReqEvaluation,ReplyEvaluation,ReqApprove,ReplyApprove}是對外不可見的 動作。

記消除 動作后的服務組合LoanService為LoanServiceOut，則：

對比可見，ReverseClient與LoanServiceOut的外部可觀察動作集完全一致，即ReverseClient與LoanServiceOut弱互模擬，所以ReverseClient與LoanServiceOut觀察等價，又LoanServiceOut與LoanService觀察等價，從而ReverseClient與LoanService是弱互模擬的，即觀察等價性成立。

利用MWB驗證工具證明：

在MWB目錄下創建LoanService.ag文件，將Client、CAS、CES、AS、ReverseClient、LoanService 的進程表達式寫入文件中。然后在命令行輸入”weq ReverseClientLoan-Service”，運行結果提示兩個進程等價，證畢。

本文簡單介紹了π演算的語法定義，給出了π演算理論形式化描述BPEL服務組合的建模算法，最后結合一個銀行信貸系統的服務組合實例，進行建模和觀察等價性驗證。π演算是進行Web服務建模驗證的有效理論工具，相信利用MWB等工具對進程表達式進行自動求逆和驗證是未來的研究熱點。

[1]MILNER R.Communicating and mobile systems:the π-calculus[M].Cambridge University Press,1999.

[2]DENG Shui Guang.Research on automatic service composition and formal verication.Zhejiang University,2007.