1、隨著Web服務(wù)數(shù)量的急劇增多，用戶面臨大量的服務(wù)選擇。因此如何從眾多功能相似的Web服務(wù)中高效地發(fā)現(xiàn)滿足條件的服務(wù)，如何判定服務(wù)組合的正確性等問題，已成為業(yè)界研究的熱點(diǎn)。其中，恰當(dāng)?shù)拿枋鯳eb服務(wù)及其組合，刻畫其相似性、組合正確性等性質(zhì)是當(dāng)前首要解決的問題。歷史上先后出現(xiàn)了大量Web服務(wù)的描述語言，然而它們大多都是非形式化的。為了更精確的描述和討論服務(wù)及其組合的性質(zhì)，本文引入形式化方法構(gòu)建了Web服務(wù)的一個(gè)理論模型，并以此為基礎(chǔ)討論了W

2、eb服務(wù)的等價(jià)性。具體來說，研究內(nèi)容主要包括以下幾個(gè)方面。 首先，本文在傳值CCS系統(tǒng)的基礎(chǔ)上，提出了SVCCS系統(tǒng)。該系統(tǒng)不僅可以描述進(jìn)程的交互行為，還能夠刻畫其結(jié)構(gòu)特點(diǎn)。在此基礎(chǔ)上，進(jìn)一步引入了互模擬的概念來討論進(jìn)程的等價(jià)性問題。考慮到進(jìn)程描述的簡潔性要求及其等價(jià)驗(yàn)證的計(jì)算復(fù)雜性要求，本文采用符號(hào)化思想將SVCCS系統(tǒng)進(jìn)一步改進(jìn)為S-系統(tǒng)，同時(shí)證明了兩者所刻畫的進(jìn)程等價(jià)關(guān)系是一致的。 其次，本文引入了一個(gè)Web服務(wù)的