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

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

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

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