鐘發(fā)榮， 吳佳杰

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

0 引 言

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

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

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

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

1 模型的語(yǔ)法

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

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

Exπ-進(jìn)程由如下語(yǔ)法定義：

其中前7個(gè)為π-演算的標(biāo)準(zhǔn)算子.下面簡(jiǎn)要介紹其他幾個(gè)算子：

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

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

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

2 模型的語(yǔ)義

Exπ-進(jìn)程上的結(jié)構(gòu)同余≡是關(guān)于α換名、并行復(fù)合封閉并且滿足如下公理的最小等價(jià)關(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(補(bǔ)償提取) 提取函數(shù)xtr(P)用于提取存儲(chǔ)于進(jìn)程P中的補(bǔ)償，歸納定義如下：

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]表明該模型支持嵌套失敗，即當(dāng)事務(wù)發(fā)生異常時(shí)，中止子事務(wù)，同時(shí)執(zhí)行子事務(wù)相應(yīng)的補(bǔ)償.

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

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

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

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

3 事務(wù)的唯一性

不同事務(wù)根據(jù)事務(wù)標(biāo)識(shí)符進(jìn)行區(qū)分，并且異常信號(hào)直接對(duì)應(yīng)事務(wù)標(biāo)識(shí)符.因此，必須為該補(bǔ)償模型定義一個(gè)簡(jiǎn)單類型系統(tǒng)，從而保證事務(wù)的唯一性.

首先規(guī)定一些符號(hào)：ti(P)表示進(jìn)程P中所有事務(wù)標(biāo)識(shí)符集;fti(P)表示進(jìn)程P中所有自由事務(wù)標(biāo)識(shí)符集;bti(P)表示進(jìn)程P中所有約束事務(wù)標(biāo)識(shí)符集.則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(良類型進(jìn)程) 若進(jìn)程P在類型假設(shè)集Γ下不出現(xiàn)任何類型錯(cuò)誤，則稱該進(jìn)程在Γ下為良類型進(jìn)程，記作Γ├P.

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

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

定義6驗(yàn)證進(jìn)程P中的事務(wù)標(biāo)識(shí)符是否唯一的謂詞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 不同補(bǔ)償模型的比較

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

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

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

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

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

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

命題1若P≈Q,則P和Q是should測(cè)試等價(jià)的.

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

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實(shí)現(xiàn)演算C1到的C2編碼：對(duì)于任意的合式進(jìn)程P，Pshould測(cè)試等價(jià)于 [[P]] .

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

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

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

命題6如果P為合式進(jìn)程，那么P≈[[P]]p2s.

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

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

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

5 結(jié) 論

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

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

參考文獻(xiàn)：

[1]唐海明.一種支持QoS約束的Web服務(wù)組合方法[D].金華：浙江師范大學(xué)數(shù)理與信息工程學(xué)院，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].北京:北京大學(xué)數(shù)學(xué)科學(xué)學(xué)院,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.