Web服務事務的動態補償模型

鐘發榮， 吳佳杰

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

0 引 言

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

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

Web服務事務的補償處理一直是Web服務的研究重點.為了支持補償處理，事務在執行過程中必須安裝相應的補償.一旦事務發生異常，可以按用戶所規定的順序執行補償，從而最大限度地消除影響.學者們嘗試研究了多個Web服務事務補償的形式化方法，包括cCSP模型[2-3]、Webπ∞模型[4]、c-BPEL模型[5]、dcπ模型[6]等.cCSP模型是基于流程的補償模型，一個動作對應一個補償進程，采用集中協調機制，但不支持移動性.Webπ∞模型是靜態定義補償的模型，事務的補償靜態地附在該事務上，并不隨著事務的執行動態地安裝相應補償，缺乏靈活性和可靠性，容易在復雜的網絡環境中發生錯誤.c-BPEL模型可看成WS-BPEL語言的抽象，是基于域的補償模型，但缺乏移動性，不能模擬隨著時間變化進而造成結構變化的系統.dcπ模型是在π-演算的基礎上定義了一個長事務的動態恢復機制,該補償機制采用了并行動態補償策略，補償的安裝和執行都采用并行方式，因此不能根據安裝的補償確定不同并行動作的執行順序.

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

1 模型的語法

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

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

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

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

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

3)隔離塊[P]中的進程P不會被外界環境中斷.當事務發生異常時，其相應補償就會置于隔離塊中執行.這個算子主要保護補償的正確安裝與執行.若隔離塊內部進程發生異常，則立即中止該隔離塊.

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

2 模型的語義

Exπ-進程上的結構同余≡是關于α換名、并行復合封閉并且滿足如下公理的最小等價關系：

(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(補償提取) 提取函數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]表明該模型支持嵌套失敗，即當事務發生異常時，中止子事務，同時執行子事務相應的補償.

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

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

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

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

3 事務的唯一性

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

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

下面給出類型系統的定義.

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

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

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

該類型系統的類型語法定義如下：

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

定義6驗證進程P中的事務標識符是否唯一的謂詞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 不同補償模型的比較

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

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

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

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

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

稱≈為最大的弱互模擬關系.

命題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實現演算C1到的C2編碼：對于任意的合式進程P，Pshould測試等價于 [[P]] .

定義11函數 [[P]]p2s實現從并行動態到靜態補償演算進程的映射，定義如下：

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

令‖P‖p2s為并行動態補償的進程到靜態補償所有可能的翻譯，它包含了從定義11的規則所得到的全部進程.其中對于事務{P;Q}n，其翻譯由以下方式進行替換：

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

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

定理3不存在編碼 [[P]]g2s，實現SExπ-演算到靜態補償演算的編碼.

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

5 結 論

本文設計了一個Web服務事務的動態補償模型——Exπ模型，該模型獨立于具體的Web服務語言和方案，是對現有模型的改進.建立這種模型的目的，是試圖把握Web服務及其事務補償的本質特征，從而更好地理解和改進Web服務的組合機制.

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

參考文獻：

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