基于進(jìn)程代數(shù)的Web服務(wù)編排方法及其類(lèi)型理論研究.pdf

1、面向服務(wù)計(jì)算是下一代基于互聯(lián)網(wǎng)的全新軟件體系結(jié)構(gòu)。它具有分布、共享、健壯、可擴(kuò)展、可移植、互操作等特性。這些特性主要來(lái)自服務(wù)的互操作特性和復(fù)合特性。面向服務(wù)計(jì)算目前主要實(shí)現(xiàn)方式是基于Web服務(wù)。Web服務(wù)是分布、獨(dú)立的代碼片斷，通過(guò)相互交換信息來(lái)完成一個(gè)特定任務(wù)。不同于傳統(tǒng)的軟件組件，Web服務(wù)可以通過(guò)互聯(lián)網(wǎng)進(jìn)行交互。Web服務(wù)的實(shí)現(xiàn)得益于Web服務(wù)標(biāo)準(zhǔn)的發(fā)布，主要是三個(gè)基礎(chǔ)協(xié)議：內(nèi)容使用格式無(wú)關(guān)的XML;網(wǎng)絡(luò)資源的命名使用URI;消息

2、的傳遞使用HTTP或SOAP。Web服務(wù)標(biāo)準(zhǔn)包括：Web服務(wù)接口描述WSDL、語(yǔ)義Web服務(wù)等。然而，Web服務(wù)實(shí)現(xiàn)復(fù)雜功能的關(guān)鍵是將功能單一的多個(gè)Web服務(wù)復(fù)合為功能復(fù)雜的Web服務(wù)。因此，Web服務(wù)中關(guān)鍵技術(shù)是Web服務(wù)復(fù)合。目前W3C等組織主要有兩種候選方案：WS-BPEL和WS-CDL。WS-CDL是交互描述語(yǔ)言，稱(chēng)為Web服務(wù)編排(Choreography)。它從全局的角度來(lái)看Web服務(wù)復(fù)合，通過(guò)WS-CDL描述可以保證多個(gè)W

3、eb服務(wù)交互的無(wú)死鎖、活鎖、公平等性質(zhì)。其WorkUnit提供模塊復(fù)用功能。WS-CDL的主要特色包括WorkUnit和基于信息對(duì)齊交互。WS-BPEL稱(chēng)為Web服務(wù)編制(Orchestration)執(zhí)行語(yǔ)言。它是從一個(gè)參與者的角度來(lái)實(shí)現(xiàn)Web服務(wù)的復(fù)合功能。
　　 Web服務(wù)標(biāo)準(zhǔn)中存在定義不嚴(yán)謹(jǐn)?shù)那闆r，即沒(méi)有給出WS-BPEL和WS-CDL的嚴(yán)謹(jǐn)語(yǔ)義，其結(jié)果可能導(dǎo)致幾個(gè)簡(jiǎn)單Web服務(wù)間復(fù)合存在不兼容的情況，這樣就有必要采用嚴(yán)密

4、的形式化方法來(lái)描述驗(yàn)證Web服務(wù)編排復(fù)合性質(zhì)。
　　 進(jìn)程代數(shù)是用代數(shù)方法對(duì)分布與并發(fā)系統(tǒng)進(jìn)行研究。進(jìn)程是進(jìn)程代數(shù)的元素，進(jìn)程代數(shù)可以通過(guò)給定公理和復(fù)合算子的方法來(lái)定義。常見(jiàn)復(fù)合算子包括：順序、并行、隨機(jī)選擇、遞歸演算。這樣就可以用功能強(qiáng)大的代數(shù)規(guī)格說(shuō)明來(lái)描述系統(tǒng)，并可以驗(yàn)證系統(tǒng)性質(zhì)。
　　 本文以Web服務(wù)編排復(fù)合方法為研究對(duì)象，以Web服務(wù)編排復(fù)合為目標(biāo)，研究基于進(jìn)程代數(shù)的Web服務(wù)編排復(fù)合關(guān)鍵方法和技術(shù)。主要貢獻(xiàn)與

5、創(chuàng)新如下：
　　 1)提出了基于進(jìn)程代數(shù)的Web服務(wù)(Process Algebra for Web Service-PA4WS)形式化模型，給出了PA4WS的語(yǔ)法模型、語(yǔ)義模型、類(lèi)型理論、子類(lèi)型關(guān)系和遞歸類(lèi)型的子類(lèi)型關(guān)系四部分。
　　 2)PA4WS語(yǔ)法模型中，和已有的研究成果相比，除常規(guī)的輸入、輸出等基本交互外，在借用服務(wù)（會(huì)話）通道概念描述基本交互基礎(chǔ)上，新增WorkUnit算子。會(huì)話是對(duì)無(wú)限制、復(fù)雜交互進(jìn)行封閉的

6、較常規(guī)抽象方法，它的引入保證了服務(wù)中的數(shù)據(jù)無(wú)關(guān)性和數(shù)據(jù)能夠被隱式創(chuàng)建；WorkUnit算子的引入可方便地描述Web服務(wù)交互的異步性質(zhì)。更重要的是，就我們所知，這是首次借助WorkUnit算子形式化描述了Web服務(wù)編排中基于信息對(duì)齊的交互。
　　 3)在PA4WS語(yǔ)義模型中，定義了其結(jié)構(gòu)化小步操作語(yǔ)義，并給出PA4WS自由變量、受囿變量、結(jié)構(gòu)化同余關(guān)系的定義、相關(guān)的代數(shù)性質(zhì)及其證明。
　　 4)在類(lèi)型理論中，基于基礎(chǔ)公理的

7、類(lèi)型描述框架，給出PA4WS類(lèi)型環(huán)境推演構(gòu)造規(guī)則、值推演規(guī)則和類(lèi)型推演規(guī)則等理論體系?；诮Y(jié)構(gòu)歸納法和規(guī)則歸納法等證明論方法給出PA4WS類(lèi)型理論的健全性檢查、進(jìn)程項(xiàng)同余關(guān)系一致性和進(jìn)程項(xiàng)歸約關(guān)系一致性等相關(guān)性質(zhì)證明。
　　 5)在子類(lèi)型關(guān)系和遞歸類(lèi)型的子類(lèi)型關(guān)系部分，基于（逆像）良基歸納法和余歸納法，證明了帶遞歸算子的子類(lèi)型關(guān)系與正則樹(shù)子類(lèi)型是一致的。
　　 6)基于javacc和vizgraph，開(kāi)發(fā)了簡(jiǎn)化版PA4W