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

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

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

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

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

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

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

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