Web服務(wù)組合的形式化建模與相容性分析.pdf

1、隨著Web服務(wù)技術(shù)的研究、發(fā)展和應(yīng)用，眾多學(xué)者試圖尋找Web服務(wù)組合驗(yàn)證的有效方法，開始運(yùn)用形式化方法描述Web服務(wù)組合并對(duì)其進(jìn)行分析。目前國(guó)內(nèi)外有使用進(jìn)程代數(shù)、petri網(wǎng)、spin等工具來(lái)形式化建模、驗(yàn)證Web服務(wù)組合語(yǔ)言，但是他們都存在某些不足，而且多限于探索或者僅停留在理論研究階段。 本文在對(duì)現(xiàn)有Web服務(wù)形式化驗(yàn)證方法的研究基礎(chǔ)上，討論了它們的特點(diǎn)和不足，并詳細(xì)分析了現(xiàn)在廣泛使用的Web服務(wù)組合語(yǔ)言標(biāo)準(zhǔn)BPEL4WS規(guī)

2、范的特性，提出了一套基于pi演算的BPEL4WS的建模規(guī)則，之后深入研究了類型系統(tǒng)理論，提出了一種切實(shí)可行的基于類型化pi演算的Web服務(wù)組合相容性分析方法。 本文的研究?jī)?nèi)容主要包括三部分：第一部分是對(duì)BPEL4WS規(guī)范形式化建模的研究，對(duì)pi演算進(jìn)行了順序算子的擴(kuò)充，給出了擴(kuò)充的語(yǔ)法和操作語(yǔ)義，并用pi演算的通信并發(fā)結(jié)構(gòu)表示BPEL4WS規(guī)范的link結(jié)構(gòu)；基于對(duì)BPEL4WS規(guī)范死路排除DPE模式的分析，提出了一個(gè)完善的解決

3、DPE問(wèn)題的pi演算形式化方法，從而系統(tǒng)地完成了從Web服務(wù)組合語(yǔ)言BPEL4WS規(guī)范到擴(kuò)充pi演算的映射；第二部分是對(duì)類型系統(tǒng)的研究，我們區(qū)分了通道的輸入輸出能力，將類型互模擬關(guān)系擴(kuò)充到了區(qū)分傳輸能力的通道類型上，并給出了相關(guān)性質(zhì)和定理的證明；我們給出了類型互模擬和子類型的關(guān)系，重新定義了類型上下文環(huán)境，給出了進(jìn)程類型定義良好的推理規(guī)則，最后定義了類型化pi演算的規(guī)約語(yǔ)義。第三部分在前面兩部分研究的基礎(chǔ)上，用類型化pi演算對(duì)BPEL4