基于π演算的BPEL組合服務(wù)的形式化描述及驗(yàn)證

夏紅星

（江蘇靖江教師進(jìn)修學(xué)校，江蘇 泰州214500）

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

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

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

1 基于π演算的BPEL服務(wù)組合建模

1.1 π演算的語法定義

π演算是由MILNER R等人在通信系統(tǒng)演算CCS的基礎(chǔ)上提出來的描述和分析通信拓?fù)浣Y(jié)構(gòu)動態(tài)變化的計算模型。設(shè)N為無限名字集，x、y等小寫字母為名字集上的名字；A、B等表示進(jìn)程；P、Q等表示進(jìn)程表達(dá)式，進(jìn)程表達(dá)式包括以下幾種形式：

0表示空進(jìn)程；P+Q表示選擇執(zhí)行P或者Q，只執(zhí)行其中一個。

(2)并發(fā)表達(dá)式：P|Q表示并發(fā)執(zhí)行進(jìn)程P、Q。

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

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

負(fù)前綴yx.P表示在端口y上輸出x后，再執(zhí)行進(jìn)程P；

.P稱為啞前綴，表示進(jìn)程外部不可見的動作，執(zhí)行完進(jìn)程后，再執(zhí)行 P。

(4)循環(huán)表達(dá)式：！P表示無窮復(fù)制進(jìn)程P。

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

(6)匹配表達(dá)式：[x=y].P表示當(dāng)條件x=y成立時才執(zhí)行進(jìn)程P。

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

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

1.2 BPEL描述的Web組合服務(wù)的π演算建模

1.2.1 建模算法

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

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

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

(3)根據(jù) Web組合服務(wù)業(yè)務(wù)流程圖，按照下表所示的Web服務(wù)元素與π演算的元素對應(yīng)關(guān)系，將業(yè)務(wù)流程圖轉(zhuǎn)換成π演算流圖。對應(yīng)關(guān)系如表1所示。

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

表1 BPEL中Web服務(wù)與π演算元素對應(yīng)關(guān)系

1.2.2 建模實(shí)例

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

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

根據(jù)建模算法，將業(yè)務(wù)流程圖抽象出如下的π演算流圖，如圖2所示。

根據(jù)π演算流圖，寫出借貸系統(tǒng)服務(wù)的建模表達(dá)式如下：

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

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

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

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

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

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

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

審批服務(wù)AS在通道Z上與信貸服務(wù)通信：

設(shè) a={Z,ReqApprove,ReplyApprove}，則：

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

2 基于π演算的BPEL組合服務(wù)的驗(yàn)證

2.1 Web服務(wù)組合內(nèi)部邏輯驗(yàn)證的內(nèi)容

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

2.2 觀察等價性和死鎖的驗(yàn)證

本文的驗(yàn)證除了手工推演，還借助了自動化π演算工具M(jìn)WB。MWB采用基于New Jersey SML語言編譯器，適用于操作和分析動態(tài)并發(fā)系統(tǒng)。

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

Client的逆進(jìn)程為：

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

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

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

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

利用MWB驗(yàn)證工具證明：

在MWB目錄下創(chuàng)建LoanService.ag文件，將Client、CAS、CES、AS、ReverseClient、LoanService 的進(jìn)程表達(dá)式寫入文件中。然后在命令行輸入”weq ReverseClientLoan-Service”，運(yùn)行結(jié)果提示兩個進(jìn)程等價，證畢。

本文簡單介紹了π演算的語法定義，給出了π演算理論形式化描述BPEL服務(wù)組合的建模算法，最后結(jié)合一個銀行信貸系統(tǒng)的服務(wù)組合實(shí)例，進(jìn)行建模和觀察等價性驗(yàn)證。π演算是進(jìn)行Web服務(wù)建模驗(yàn)證的有效理論工具，相信利用MWB等工具對進(jìn)程表達(dá)式進(jìn)行自動求逆和驗(yàn)證是未來的研究熱點(diǎn)。

[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.