鐘發(fā)榮， 吳佳杰

(浙江師范大學 數(shù)理與信息工程學院,浙江 金華 321004)

0 引 言

Web服務(wù)技術(shù)具有良好的互操作性、跨平臺性及松散耦合的特點，能夠為不同實現(xiàn)標準和不同通信機制下的軟件系統(tǒng)的交互與集成提供有效支持.然而在多數(shù)情況下，單個服務(wù)不能滿足復(fù)雜的功能要求，有必要把現(xiàn)有的、可能是異構(gòu)的Web服務(wù)組裝在一起，為用戶提供增值服務(wù)[1].Web服務(wù)組合能夠?qū)崿F(xiàn)快速組合和自適應(yīng)，同時也是能讓用戶持續(xù)使用運行的軟件系統(tǒng)，因此，被廣泛應(yīng)用于改進企業(yè)軟件系統(tǒng)的敏捷性、靈活性和可用性等方面.

Web服務(wù)組合通常是松散耦合、跨平臺的，運行時間長，容易受到各種故障的影響.現(xiàn)有的基于XML的Web服務(wù)工業(yè)標準為解決Web服務(wù)在復(fù)雜的異構(gòu)環(huán)境下實現(xiàn)松散耦合的消息傳遞和協(xié)同操作提供了基礎(chǔ)，但缺乏對安全控制的支持，從而無法保證Web服務(wù)在執(zhí)行過程中的安全性和可靠性.事務(wù)是提高系統(tǒng)可靠性的一種有效手段，為保證在遇到故障的情況下仍能正確執(zhí)行組合Web服務(wù)，Web服務(wù)必須支持事務(wù)處理，從而保證服務(wù)在異構(gòu)環(huán)境下的可靠性.然而,Web服務(wù)中的事務(wù)不同于經(jīng)典的ACID事務(wù)，不能采用資源鎖定策略.一般情況下，當Web服務(wù)事務(wù)失敗時，不是簡單地通過回滾消除影響，而是通過特定流程最大限度地消除影響，這種特定流程被稱為“補償”.

Web服務(wù)事務(wù)的補償處理一直是Web服務(wù)的研究重點.為了支持補償處理，事務(wù)在執(zhí)行過程中必須安裝相應(yīng)的補償.一旦事務(wù)發(fā)生異常，可以按用戶所規(guī)定的順序執(zhí)行補償，從而最大限度地消除影響.學者們嘗試研究了多個Web服務(wù)事務(wù)補償?shù)男问交椒?，包括cCSP模型[2-3]、Webπ∞模型[4]、c-BPEL模型[5]、dcπ模型[6]等.cCSP模型是基于流程的補償模型，一個動作對應(yīng)一個補償進程，采用集中協(xié)調(diào)機制，但不支持移動性.Webπ∞模型是靜態(tài)定義補償?shù)哪Ｐ?，事?wù)的補償靜態(tài)地附在該事務(wù)上，并不隨著事務(wù)的執(zhí)行動態(tài)地安裝相應(yīng)補償，缺乏靈活性和可靠性，容易在復(fù)雜的網(wǎng)絡(luò)環(huán)境中發(fā)生錯誤.c-BPEL模型可看成WS-BPEL語言的抽象，是基于域的補償模型，但缺乏移動性，不能模擬隨著時間變化進而造成結(jié)構(gòu)變化的系統(tǒng).dcπ模型是在π-演算的基礎(chǔ)上定義了一個長事務(wù)的動態(tài)恢復(fù)機制,該補償機制采用了并行動態(tài)補償策略，補償?shù)陌惭b和執(zhí)行都采用并行方式，因此不能根據(jù)安裝的補償確定不同并行動作的執(zhí)行順序.

基于進程代數(shù)的形式化方法允許對基于消息通信的并發(fā)系統(tǒng)進行建模和分析，可以自然地應(yīng)用到Web服務(wù)的建模和開發(fā)之中.以π-演算[7]為代表的移動進程演算可以清晰地定義Web服務(wù)中的控制流程，模擬Web服務(wù)之間的交互，描述結(jié)構(gòu)不斷變化的Web服務(wù)系統(tǒng).因此，本文選用π-演算作為形式化工具來研究Web服務(wù)及事務(wù)的補償.

1 模型的語法

本文對π-演算進行擴展，定義了作為Web服務(wù)事務(wù)補償模型的Exπ-演算.在該模型中，Web服務(wù)事務(wù)的補償可以靜態(tài)或動態(tài)地定義和安裝：1)補償進程可隨著Web服務(wù)的交互而動態(tài)地安裝起來;2)事務(wù)可靜態(tài)地定義其補償.

設(shè)N為無窮名字集，其元素用小寫字母如a,b,c,…表示，指所有的通道名;用大寫字母如P,Q,R,…等表示進程，X,Y,Z,…等表示進程變量.

Exπ-進程由如下語法定義：

其中前7個為π-演算的標準算子.下面簡要介紹其他幾個算子：

1){P;R}n是名為n的事務(wù)，P和R分別為事務(wù)的主體進程和補償進程.事務(wù)在正常情況下執(zhí)行主體進程P，一旦發(fā)生異常，中止主體進程P并激活該事務(wù)的補償進程R.若整個事務(wù)直至完成都未曾發(fā)生異常，那么其補償進程就會自動地安裝到父事務(wù)中，同時該事務(wù)將被垃圾回收.

3)隔離塊[P]中的進程P不會被外界環(huán)境中斷.當事務(wù)發(fā)生異常時，其相應(yīng)補償就會置于隔離塊中執(zhí)行.這個算子主要保護補償?shù)恼_安裝與執(zhí)行.若隔離塊內(nèi)部進程發(fā)生異常，則立即中止該隔離塊.

Exπ-進程中的名字分為自由名和約束名.用fn(P)表示進程P的自由名集；bn(P)表示進程P的約束名集.

2 模型的語義

Exπ-進程上的結(jié)構(gòu)同余≡是關(guān)于α換名、并行復(fù)合封閉并且滿足如下公理的最小等價關(guān)系：

(vx)0≡0;(vx)(vy)P≡(vy)(vx)P;P|(vx)Q≡(vx)(P|Q) ifx?fn(P);

P+(vx)Q≡(vx)(P+Q) ifx?fn(P);{(vx)P;R}n≡(vx){P;R}nifx?fn(R)∩{n};

定義1(補償提取) 提取函數(shù)xtr(P)用于提取存儲于進程P中的補償，歸納定義如下：

xtr(P|Q)=xtr(P)|xtr(Q);xtr(P+Q)=xtr(P)+xtr(Q);xtr((vx)P)=(vx)xtr(P);

xtr([P])=[P];xtr({P;R}n)=xtr(P)|[R].

xtr({P;R}n)=xtr(P)|[R]表明該模型支持嵌套失敗，即當事務(wù)發(fā)生異常時，中止子事務(wù)，同時執(zhí)行子事務(wù)相應(yīng)的補償.

定義2(輸入謂詞) 用于檢查進程是否不包含輸入動作的謂詞inp(P)，歸納定義如下：

inp(P+Q) ifinp(P) andinp(Q);inp(P|Q) ifinp(P) andinp(Q).

如果inp(P)為真，則進程P是活的，因此事務(wù){(diào)P;R}n可以發(fā)生異常；反之，如果inp(P)為假，則進程P是非活的，因此事務(wù){(diào)P;R}n是已成功提交的，不會發(fā)生任何異常.

很多靜態(tài)補償只能補償正在執(zhí)行的事務(wù)，當事務(wù)成功提交后，相應(yīng)補償就被垃圾回收.補償已經(jīng)成功完成的事務(wù)需要通過復(fù)雜的機制才能實現(xiàn),但本模型卻可通過帶補償更新的輸入操作，簡單地將已成功完成的子事務(wù)的補償安裝到其父事務(wù)的補償進程中.子事務(wù)和父事務(wù)之間使用一個特定通道，當子事務(wù)成功完成時，該通道將其補償傳遞給父事務(wù)，父事務(wù)可通過輸入操作激活補償更新，從而將補償進程安裝到父事務(wù)中.

3 事務(wù)的唯一性

不同事務(wù)根據(jù)事務(wù)標識符進行區(qū)分，并且異常信號直接對應(yīng)事務(wù)標識符.因此，必須為該補償模型定義一個簡單類型系統(tǒng)，從而保證事務(wù)的唯一性.

首先規(guī)定一些符號：ti(P)表示進程P中所有事務(wù)標識符集;fti(P)表示進程P中所有自由事務(wù)標識符集;bti(P)表示進程P中所有約束事務(wù)標識符集.則fti(P)=ti(P)ti(P).

下面給出類型系統(tǒng)的定義.

定義3給名x指定類型T，稱為類型假設(shè)，記作x:T.一組有限的類型假設(shè)稱為類型假設(shè)集，記作Γ.Γ,x:T表示向類型假設(shè)集Γ中加入新類型假設(shè)x:T.

定義4(類型函數(shù))Γ(x)=T是指在類型假設(shè)集Γ下，名x到類型T的映射函數(shù).

定義5(良類型進程) 若進程P在類型假設(shè)集Γ下不出現(xiàn)任何類型錯誤，則稱該進程在Γ下為良類型進程，記作Γ├P.

該類型系統(tǒng)的類型語法定義如下：

定理1(服從歸約) 若Γ├P,P→P′，則Γ├P′.

定義6驗證進程P中的事務(wù)標識符是否唯一的謂詞unq(P)定義如下：

unq([P]) ifunq(P);unq(P+Q) ifunq(P)∧unq(Q);

unq({P;Q}n) ifunq(P)∧unq(Q)∧n?fti(P);

定理2如果Γ├P，那么一定有unq(P).

4 不同補償模型的比較

下面比較靜態(tài)補償、并行動態(tài)補償和Exπ-演算的表達能力.為了便于研究這3類補償模型的關(guān)系，本文簡化了Exπ-演算的補償更新操作：任意進程都可觸發(fā)補償更新操作λX.Q，而無需通過輸入觸發(fā)λX.Q.稱簡化的Exπ-演算為SExπ-演算，其進程的語法定義如下：

式中:CTi,j(t-1)為前一個周期,節(jié)點i對j的的綜合信任值。λ為前一周期的綜合信任值的權(quán)重,即歷史信任的權(quán)重。

如果補償更新的形式為[λX.(X|Q)].P，且進程變量X不屬于Q，那么應(yīng)用該補償更新時，進程Q作為補償并行地安裝到事務(wù)中，以這種方式更新補償?shù)哪Ｐ头Q為并行動態(tài)補償模型.而靜態(tài)補償模型沒有補償更新操作.因此，該語法已經(jīng)包含了靜態(tài)與并行動態(tài)模型的語法，其操作語義也包含在SExπ-模型中.

定義7(弱互模擬) 令R為進程上的對稱二元關(guān)系.稱R為弱互模擬，若PRQ，則蘊含：

4)如果xtr(Q)?Q′，那么xtr(P)RQ′.

稱≈為最大的弱互模擬關(guān)系.

命題1若P≈Q,則P和Q是should測試等價的.

定義9(合式進程) 合式謂詞wf(P)用于校驗進程P是否為合式進程，定義如下：

wf((vx)P) ifwf(P);wf(P|Q) ifwf(P) andwf(Q);wf(P+Q) ifwf(P) andwf(Q);

wf([P]) ifwf(P);wf([λX.Q].P) ifwf(P) andwf(Q);wf({P;R}n) ifwf(P) andwf(Q).

定義10(編碼) [[5]]:C1→C2實現(xiàn)演算C1到的C2編碼：對于任意的合式進程P，Pshould測試等價于 [[P]] .

定義11函數(shù) [[P]]p2s實現(xiàn)從并行動態(tài)到靜態(tài)補償演算進程的映射，定義如下：

[[P+Q]]p2s=[[P]]p2s+[[Q]]p2s; [[(vx)P]]p2s=(vx)[[P]]p2s; [[[P]]]p2s=[[[P]]p2s];

令‖P‖p2s為并行動態(tài)補償?shù)倪M程到靜態(tài)補償所有可能的翻譯，它包含了從定義11的規(guī)則所得到的全部進程.其中對于事務(wù){(diào)P;Q}n，其翻譯由以下方式進行替換：

命題6如果P為合式進程，那么P≈[[P]]p2s.

由命題1知，若P≈[[P]]p2s,則P和 [[P]]p2s是should測試等價的.因此，對于合式進程P，Pshould測試等價于 [[P]]p2s， 即符合 [[P]]p2s的編碼條件.由SExπ-進程的定義，可以將靜態(tài)補償編碼成并行動態(tài)補償演算.因此，靜態(tài)補償模型和并行動態(tài)模型具有相同的表達能力.

定理3不存在編碼 [[P]]g2s，實現(xiàn)SExπ-演算到靜態(tài)補償演算的編碼.

顯然，可以將靜態(tài)補償編碼成SExπ，結(jié)合定理3，SExπ模型的表達能力要大于靜態(tài)補償模型.進而本演算比靜態(tài)和并行動態(tài)演算更靈活、表達能力更強.

5 結(jié) 論

本文設(shè)計了一個Web服務(wù)事務(wù)的動態(tài)補償模型——Exπ模型，該模型獨立于具體的Web服務(wù)語言和方案，是對現(xiàn)有模型的改進.建立這種模型的目的，是試圖把握Web服務(wù)及其事務(wù)補償?shù)谋举|(zhì)特征，從而更好地理解和改進Web服務(wù)的組合機制.

Exπ模型可以靜態(tài)或動態(tài)地定義和安裝補償進程，更具有靈活性.一方面，補償進程可隨著Web服務(wù)之間的交互而動態(tài)地安裝起來；另一方面，事務(wù)也可靜態(tài)地定義該事務(wù)的補償.本文為該模型增加了一個簡單的類型系統(tǒng)，保證了事務(wù)的唯一性.最后，對幾類補償模型進行統(tǒng)一的形式化定義，通過與其他補償模型的比較，充分展示了該模型的靈活性和表達能力.

參考文獻：

[1]唐海明.一種支持QoS約束的Web服務(wù)組合方法[D].金華：浙江師范大學數(shù)理與信息工程學院，2009.

[2]Butler M J,Hoare T,Ferrera C.A Trace Semantics for Long-Running Transaction[C]//Lecture Notes in Computer Science.Berlin:Springer,2005:133-150.

[3]Butler M J,Ripon S.Executable Semantics for Compensating CSP[C]//Lecture Notes in Computer Science.Berlin:Springer,2005:243-256.

[4]Mazzara M,Lucchi R.A Framework for Generic Error Handling in Business Processes[J].Electronic Notes in Theoretical Computer Science,2004,105:133-145.

[5]趙翔鵬.Web服務(wù)組合的建模和分析[D].北京:北京大學數(shù)學科學學院,2008.

[6]Vaz C,Ferreira C,Ravara A.Dynamic Recovering of Long Running Transactions[C]//Lecture Notes in Computer Science.Berlin:Springer,2009:201-215

[7] Milner R.Communicating and Mobile Systems:the π-Calculus[M].Cambridge:Cambridge University Press,1999.