Webπ-,∞-行為理論的研究.pdf

1、近年來，Web 服務(wù)研究領(lǐng)域的一個(gè)重要研究方向是探討如何組合已有的Web 服務(wù)并協(xié)調(diào)其運(yùn)行以便于更有效地利用網(wǎng)絡(luò)上已有的服務(wù)。為此，人們提出了很多Web 服務(wù)編排語言。
　　 在已經(jīng)出現(xiàn)的若干編排語言中WS-BPEL 最有可能成為該領(lǐng)域的標(biāo)準(zhǔn)。WS-BPEL 利用長期運(yùn)行事務(wù)和補(bǔ)償這兩個(gè)概念對(duì)錯(cuò)誤進(jìn)行了處理。
　　 為了形式化地刻畫WS-BPEL，Manuel Mazzara和Ivan Lanese 提出了一種新的進(jìn)程演

2、算系統(tǒng)Web π∞。Manuel Mazzara和Ivan Lanese 給出了Web π∞的歸約語義和LTS 語義，并在此基礎(chǔ)上分別定義了弱B- 同余(Weak Barbed Congruence）和封閉互模擬(Closedbisimilarity)，并證明了封閉互模擬相對(duì)弱B-同余的可靠性。但由于α? 不是圖像有限的，目前還未得到一個(gè)完備性的結(jié)果。本文主要探討在強(qiáng)情形下Web π∞的行為理論，研究內(nèi)容包括：
　　 (1）討論

3、了強(qiáng)情形下相關(guān)概念及基本性質(zhì)，包括進(jìn)程上的強(qiáng)B-同余關(guān)系，強(qiáng)封閉互模擬ca。
　　 (2）引入了一個(gè)安全函數(shù)，基于該函數(shù)定義了Up-To上下文的強(qiáng)封閉互模擬關(guān)系，進(jìn)而給出了強(qiáng)封閉互模擬ca的一個(gè)Up-To 證明技術(shù)。
　　 (3）利用上述的Up-To 證明技術(shù)，證明了強(qiáng)封閉互模擬相對(duì)于強(qiáng)B-同余的可靠性。
　　 (4）證明了α ??→的圖像有限性，在此基礎(chǔ)上完成了強(qiáng)封閉互模擬ca相對(duì)于強(qiáng)B-同余的完備性定理的證明