基于π-演算的Web服務(wù)事務(wù)補(bǔ)償模型的研究.pdf

1、隨著網(wǎng)絡(luò)的普及和Web技術(shù)的迅速發(fā)展,人們迫切需要在Internet上實(shí)現(xiàn)跨平臺(tái)、語言獨(dú)立、松散耦合的異構(gòu)應(yīng)用的集成和交互,這對傳統(tǒng)的分布式計(jì)算技術(shù)提出了新的要求。Web服務(wù)作為一種新型的分布式計(jì)算模型應(yīng)運(yùn)而生,成為網(wǎng)絡(luò)上數(shù)據(jù)和信息集成的有效機(jī)制。
　　 服務(wù)組合是將現(xiàn)有的可用Web服務(wù)組合起來、協(xié)同執(zhí)行,形成功能更強(qiáng)大的增值服務(wù)。為了滿足不同Web服務(wù)之間運(yùn)行結(jié)果的一致性和可靠性要求,我們需要在Web服務(wù)組合中提供事務(wù)處理的支

2、持。Web服務(wù)事務(wù)不同于傳統(tǒng)的ACID事務(wù),不能通過簡單回滾來恢復(fù)已完成的動(dòng)作,因此,需要采用補(bǔ)償機(jī)制來保證數(shù)據(jù)的一致性。按照不同的補(bǔ)償安裝方式,可將補(bǔ)償模型分為靜態(tài)和動(dòng)態(tài)補(bǔ)償模型。靜態(tài)補(bǔ)償模型的補(bǔ)償不是隨著事務(wù)的執(zhí)行而動(dòng)態(tài)安裝的,因此這種方法缺乏靈活性,容易在復(fù)雜的網(wǎng)絡(luò)環(huán)境中發(fā)生錯(cuò)誤。而很多動(dòng)態(tài)補(bǔ)償模型是基于流的,即采用集中式的協(xié)調(diào)機(jī)制,缺乏移動(dòng)性,不能有效地模擬結(jié)構(gòu)不斷變化的Web服務(wù)系統(tǒng)。盡管目前存在著多種補(bǔ)償模型,但他們之間的關(guān)

3、系并不是很清楚,而且表達(dá)能力的比較分析工作才剛剛起步。
　　 隨著Web服務(wù)的發(fā)展,使用形式化方法研究Web服務(wù)已成為一個(gè)重要研究內(nèi)容。其中以π-演算為代表的移動(dòng)進(jìn)程演算,比較適合研究交互服務(wù)的行為,因此可以很自然地應(yīng)用于Web服務(wù)的建模和開發(fā)之中。本文的工作主要圍繞Web服務(wù)事務(wù)及其補(bǔ)償處理的形式化研究而展開的。
　　 本文的主要研究內(nèi)容及成果如下:
　　 1.建立了一般動(dòng)態(tài)的Web服務(wù)事務(wù)補(bǔ)償模型
　　

4、 通過{P；R}n、(n)、[P]及a(x)％[λX.Q].P對標(biāo)準(zhǔn)的π-演算進(jìn)行擴(kuò)展,定義Exπ演算作為Web服務(wù)事務(wù)的一般動(dòng)態(tài)補(bǔ)償模型,同時(shí)給出了相應(yīng)的操作語義。該模型的輸入動(dòng)作可以激活補(bǔ)償更新,因此補(bǔ)償進(jìn)程可以隨著事務(wù)的交互而動(dòng)態(tài)安裝起來.為保證事務(wù)的唯一性,我們在該模型中增加了一個(gè)簡單類型系統(tǒng)。通過該補(bǔ)償演算對Web服務(wù)實(shí)例的形式化描述,充分展示了該模型的靈活性和表達(dá)能力。該模型獨(dú)立于具體的Web服務(wù)語言和方案,可以使我們更好

5、地理解和把握Web服務(wù)及其事務(wù)補(bǔ)償?shù)谋举|(zhì)特征。
　　 2.比較不同補(bǔ)償模型的表達(dá)能力
　　 用擴(kuò)展的π-演算對靜態(tài)、并行動(dòng)態(tài)和一般動(dòng)態(tài)補(bǔ)償模型進(jìn)行統(tǒng)一的形式化描述。簡化Exπ演算使得任意動(dòng)作都可以激活補(bǔ)償更新,我們稱其為點(diǎn)Exπ′模型。遞增地定義了這三類補(bǔ)償模型的語法,同時(shí)給出了相應(yīng)的操作語義。本文定義了演算的編碼條件,提出了弱互模擬關(guān)系和should測試等價(jià)概念。我們將并行動(dòng)態(tài)編碼成靜態(tài)補(bǔ)償演算,證明了靜態(tài)和并行動(dòng)態(tài)補(bǔ)