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

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

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

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

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

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

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

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