基于π-演算的Web服務(wù)組合的建模與驗證.pdf

1、Web服務(wù)組合是一種基于面向服務(wù)架構(gòu)的技術(shù)，通過把功能單一的單個Web服務(wù)組合起來，實現(xiàn)了服務(wù)的重用與增值，解決了互聯(lián)網(wǎng)異構(gòu)應(yīng)用的集成和協(xié)作問題。Web服務(wù)組合的特點包括松耦合，行業(yè)支持，高度可集成等。
　　 Web服務(wù)組合過程非常復(fù)雜，涉及多個Web服務(wù)的通信協(xié)作，導(dǎo)致對Web服務(wù)組合的正確性驗證將是十分困難的。但是服務(wù)組合的正確性問題決定了Web服務(wù)組合能否被正確的實施，錯誤的實施則會給企業(yè)帶來嚴(yán)重的損失，所以在Web服務(wù)組

2、合被正式實施以前對其進行正確性驗證是必須的。目前描述Web服務(wù)組合的語言使用最為廣泛的是WSFL、XLANG、WS-CDL、BPEL等，它們有一個共同的缺點，缺乏形式化的工具對其進行正確性驗證。所以對Web服務(wù)組合如何進行形式化的建模，以及如何驗證模型的正確性成為Web服務(wù)組合研究領(lǐng)域的一個重要問題。
　　 對形式化建模方法進行了大量研究后，本文提出了一種基于π-演算的Web服務(wù)組合的建模方法，并對模型進行驗證工作，研究成果包括

3、以下三個方面：
　　 (1)基于π-演算的BPEL業(yè)務(wù)流程的建模
　　 本文給出了BPEL一系列關(guān)鍵元素到π-演算的建模方法，實現(xiàn)了π-演算對BPEL的自動化建模。
　　 (2)基于π-演算的BPEL業(yè)務(wù)流程模型驗證
　　 本文給出了對模型的死鎖驗證、活鎖驗證、可達性驗證等模型正確性驗證的算法，實現(xiàn)了對Web服務(wù)組合的正確性驗證。
　　 (3)WMV工具的設(shè)計與實現(xiàn)
　　 本文設(shè)計并實現(xiàn)了