Web服務(wù)組合形式化模型研究.pdf

1、隨著Web服務(wù)技術(shù)的迅速發(fā)展，越來越多的的Web服務(wù)運(yùn)行在Internet上，但單個(gè)的Web服務(wù)功能有限，難以滿足日益增長和不斷變化的用戶需求。因此，如何將已有的、運(yùn)行在異構(gòu)平臺(tái)上的Web服務(wù)組合起來，以提供給用戶更為強(qiáng)大和增值的功能，成為Web服務(wù)研究領(lǐng)域中的一個(gè)熱點(diǎn)。
　　 由于已有的Web服務(wù)可能是彼此獨(dú)立地開發(fā)，以不同語言實(shí)現(xiàn)，運(yùn)行在不同的、異構(gòu)的平臺(tái)上，因此Web服務(wù)組合存在的問題有：如何描述Web服務(wù)的動(dòng)態(tài)行為，如何

2、定義和描述Web服務(wù)間的交互的邏輯順序以保證Web服務(wù)的動(dòng)態(tài)行為的匹配性，如何保證Web服務(wù)之間傳遞消息的數(shù)據(jù)類型的一致性，如何對(duì)組合的Web服務(wù)進(jìn)行驗(yàn)證和測(cè)試以確保執(zhí)行結(jié)果的正確性。
　　 目前已經(jīng)提出的Web服務(wù)組合規(guī)范如BPEL4WS、WS-CDL都是基于XML的描述性語言，缺乏一種形式化模型來表達(dá)語言的語義以及形式化驗(yàn)證方法來保證用這些規(guī)范所定義的Web服務(wù)組合的正確性。同時(shí)，由于參與Web服務(wù)組合的各個(gè)子服務(wù)都運(yùn)行在分

3、布式異構(gòu)的環(huán)境下，因此想依靠組合的Web服務(wù)的實(shí)際運(yùn)行來檢測(cè)組合中的錯(cuò)誤是代價(jià)昂貴的并且?guī)缀跏遣豢赡艿?，因此?duì)Web服務(wù)組合的形式化驗(yàn)證也是必須的而且是非常重要的。
　　 解決上述問題的一個(gè)行之有效的辦法就是針對(duì)Web服務(wù)組合規(guī)范如BPEL4WS、WS-CDL建立合適的形式化模型，形式化地定義和描述Web服務(wù)組合的動(dòng)態(tài)交互行為，利用Web服務(wù)組合的形式化模型對(duì)Web服務(wù)組合的性質(zhì)如死鎖避免、數(shù)據(jù)類型一致性和動(dòng)態(tài)行為的匹配性進(jìn)行檢

4、查和驗(yàn)證，以保證Web服務(wù)組合的動(dòng)態(tài)行為的匹配和數(shù)據(jù)類型的一致性。
　　 因此，針對(duì)Web服務(wù)組合規(guī)范BPEL4WS和WS-CDL，研究了基于工作流的Web服務(wù)組合形式化模型以及如何利用Web服務(wù)組合的形式化模型對(duì)Web服務(wù)組合的動(dòng)態(tài)行為的匹配和數(shù)據(jù)類型的一致性進(jìn)行驗(yàn)證。
　　 針對(duì)Web服務(wù)組合規(guī)范BPEL4WS，分別建立了BPEL4WS到Pi-演算和CSP的概念映射，在此基礎(chǔ)上，建立了基于Pi-演算和CSP的BPEL

5、4WS形式化模型；同時(shí)給出了從BPEL4WS到Pi-演算和CSP進(jìn)程的自動(dòng)轉(zhuǎn)換算法和模型的驗(yàn)證方法。
　　 針對(duì)Web服務(wù)組合規(guī)范WS-CDL，建立了基于全局的形式化模型框架Abstract WS-CDL，在此基礎(chǔ)上利用Abstract WS-CDL對(duì)WS-CDL中各類行為進(jìn)行了形式化描述；同時(shí)定義了將全局模型框架Abstract WS-CDL映射到基于Pi-演算的局部BPEL4WS模型的映射規(guī)則，并給出了全局模型框架和局部模型

6、一致性的形式化定義；然后給出了全局和局部二個(gè)層次的模型驗(yàn)證方法以及全局模型框架和局部模型一致性的驗(yàn)證方法。
　　 利用基于Pi-演算的形式化方法研究和給出了二個(gè)Web服務(wù)的強(qiáng)互相容和弱互相容的形式化定義，在二個(gè)Web服務(wù)弱互相容定義的基礎(chǔ)上，定義了二個(gè)Web服務(wù)之間互投影的算法，進(jìn)而給出了多個(gè)Web服務(wù)互相容的形式化定義；然后給出了Web服務(wù)的可替換性的判斷準(zhǔn)則和二個(gè)Web服務(wù)相容性的檢測(cè)算法。
　　 研究和給出了類型化

7、的BPEL4WS形式化模型和類型化的Abstract WS-CDL形式化模型框架，特別是提出了進(jìn)程類型假設(shè)集的外延和進(jìn)程類型假設(shè)集相容性的概念，并且給出了進(jìn)程類型假設(shè)集的合并算法；在此基礎(chǔ)上，定義了全局會(huì)話和局部進(jìn)程類型良好性的推理規(guī)則和捕獲由于類型不一致而導(dǎo)致運(yùn)行時(shí)錯(cuò)誤的操作語義。同時(shí)，給出了從類型化的全局模型框架到類型化的局部模型的映射規(guī)則；然后，針對(duì)類型化的Abstract WS-CDL，給出了全局會(huì)話類型安全性質(zhì)的證明。