Web服務(wù)事務(wù)處理研究與實(shí)現(xiàn).pdf

1、Web服務(wù)事務(wù)處理必須保證多個(gè)Web服務(wù)運(yùn)行結(jié)果的可靠性和一致性，并能及時(shí)解決運(yùn)行時(shí)發(fā)生的各種異常。目前已有的Web服務(wù)事務(wù)協(xié)議均不能提供確切的事務(wù)處理語(yǔ)義定義，嚴(yán)重阻礙了事務(wù)的實(shí)現(xiàn)，例如：由IBM和Microsoft制定的WS-Coordination、WS-AT和WS-BA協(xié)議，以及由OASIS組織制定的BTP。這些規(guī)范放松了傳統(tǒng)事務(wù)中的ACID屬性的限制，重新定義了松耦合環(huán)境下的事務(wù)性質(zhì)。但是，這些規(guī)范中存在一些問(wèn)題，比如描述的不

2、詳細(xì)，有歧義等。因此，在規(guī)范的實(shí)施中，迫切需要對(duì)這些事務(wù)協(xié)議進(jìn)行形式化分析及驗(yàn)證，進(jìn)一步完善這些規(guī)范，保證協(xié)議的正確實(shí)施。本文基于多元л演算，對(duì)Web服務(wù)事務(wù)協(xié)議：WS-AT和WS-BA進(jìn)行了深入的研究，并提出了一個(gè)事務(wù)工作流的實(shí)現(xiàn)框架。 1.分析了事務(wù)的分類(lèi)，按時(shí)間順序可分為傳統(tǒng)事務(wù)、移動(dòng)事務(wù)和Web服務(wù)事務(wù)等；總結(jié)了事務(wù)的形式化研究現(xiàn)狀，根據(jù)采用的語(yǔ)言可以分為三大方法：基于Petri網(wǎng)的形式化方法、基于進(jìn)程代數(shù)的形式化方法和

3、基于時(shí)序邏輯的形式化方法，并總結(jié)了每一種方法的優(yōu)缺點(diǎn)；對(duì)Web服務(wù)事務(wù)實(shí)現(xiàn)的研究現(xiàn)狀也作了深入地調(diào)查。 2.由于WS-AT采用簡(jiǎn)單的狀態(tài)轉(zhuǎn)換圖和狀態(tài)轉(zhuǎn)換表，無(wú)法描述協(xié)調(diào)者和多個(gè)參與者的復(fù)雜協(xié)調(diào)活動(dòng)，因此為規(guī)范協(xié)調(diào)行為，用л演算給出了WS-AT的形式化描述，并采用MWB工具的弱互模擬檢驗(yàn)命令證明了WS-AT滿(mǎn)足原子性。 3.由于WS-BA也是采用簡(jiǎn)單的狀態(tài)轉(zhuǎn)換圖和狀態(tài)轉(zhuǎn)換表，并且沒(méi)有給出內(nèi)部狀態(tài)的轉(zhuǎn)變，導(dǎo)致當(dāng)有多個(gè)參與者時(shí)

4、，協(xié)調(diào)者不知如何協(xié)調(diào)它們的輸出結(jié)果，為此提出了WS-BA中參與者主動(dòng)提交協(xié)議的擴(kuò)展：BAPC。用多元л演算建立了BAPC協(xié)議的形式化模型，并證明了BAPC協(xié)議滿(mǎn)足長(zhǎng)事務(wù)協(xié)議所具有的持久性、可終止性和局部原子性。 4.根據(jù)WS-AT和WS-BA的形式化分析，在已有Web服務(wù)組合工作流引擎WebJetFlow上提出了事務(wù)工作流實(shí)現(xiàn)框架：TxWebJetFlow。通過(guò)擴(kuò)展業(yè)務(wù)流程可執(zhí)行語(yǔ)言BPEL和WebJefflow的原有數(shù)據(jù)結(jié)構(gòu)，