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

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

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

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

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

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