基于Pi-演算的Web服務形式化描述模型.pdf

1、基于基于Pi演算的演算的Web服務形式化描述模型服務形式化描述模型PiCalulusbasedFmalDeionModelfWebServices一級學科：計算機科學與技術學科專業(yè)：計算機應用技術研究生：胡靜指導教師：馮志勇教授天津大學計算機科學與技術學院二零一零年十二月中文摘要中文摘要Web服務組合使得開發(fā)者可以基于面向服務的計算無縫地訪問眾多分布式服務，組合在一起解決復雜問題。大多數(shù)Web服務是獨立開發(fā)并運行在異構(gòu)平臺上的，為了能夠

2、實現(xiàn)它們之間的服務組合，需要能夠兼容其異構(gòu)性的服務組合描述方法以及對組合后的服務進行驗證或測試的方法。本文在總結(jié)以前的研究結(jié)果的基礎上，以Pi演算為基礎，建立了Web服務形式化描述模型PiFM4WS，對Web服務以及Web服務組合的主要行為進行描述，為Web服務組合的動態(tài)體系結(jié)構(gòu)提供統(tǒng)一的描述方法；將基于不同視角的Web服務組合描述規(guī)范的主要行為映射到PiFM4WS中，說明經(jīng)過映射之后的兩類描述規(guī)范具有等價性；將類型系統(tǒng)加入PiFM4W

3、S模型中，細化了Web服務的相容性，提出可替換性的概念和驗證方法；在PiFM4WS模型中對服務網(wǎng)絡進行描述，為實現(xiàn)Web服務組合的自動化提供理論基礎。本文所取得的主要研究成果如下：(1)建立Web服務形式化描述模型PiFM4WS：給出Web服務外部和內(nèi)部行為的描述，即PiFM4WS的語法結(jié)構(gòu)定義；給出Web服務經(jīng)由交互發(fā)生組合的行為，即PiFM4WS的同構(gòu)規(guī)則和操作語義。(2)為兩類基于不同視角的描述規(guī)范的主要行為提供映射規(guī)則：為BPE

4、L4WS規(guī)范以及WSCDL規(guī)范的概念和各類行為提供PiFM4WS的描述方法，從語法定義和操作語義的角度說明兩類不同規(guī)范的等價性，并指出PiFM4WS提供的對動態(tài)體系結(jié)構(gòu)的描述方法是現(xiàn)有描述規(guī)范無法實現(xiàn)的。(3)基于類型化PiFM4WS的Web服務組合驗證：將類型系統(tǒng)加入PiFM4WS中，根據(jù)子類型的關系細化Web服務的相容性，給出Web服務的可替換性的定義；根據(jù)信道是否和業(yè)務流程相關進行分類，結(jié)合Pi演算中的代換算法，提出在動態(tài)體系結(jié)構(gòu)

5、下的Web服務可替換性的驗證方法。(4)對服務網(wǎng)絡進行形式化描述，為實現(xiàn)Web服務自動組合提供理論基礎：將抽象服務和具體服務之間的通信信道進行結(jié)構(gòu)的抽象和描述，為服務關系的形式化描述建立理論基礎。綜上所述，本文提出的形式化描述模型PiFM4WS、類型化的PiFM4WS以及服務網(wǎng)絡的形式化描述，為Web服務組合提供了統(tǒng)一的形式化描述和驗證框架，為實現(xiàn)Web服務的自動組合和驗證提供了理論基礎。關鍵詞：關鍵詞：SOCpi演算形式化描述模型We