基于BMC的Web服務(wù)失配檢測(cè)方法研究.pdf

1、面向服務(wù)的體系結(jié)構(gòu)(SOA)作為一種新的軟件開發(fā)范型，正逐步成為未來軟件發(fā)展的趨勢(shì)之一，而其主流的實(shí)現(xiàn)方式Web服務(wù)技術(shù)也得到了快速的發(fā)展與應(yīng)用。由于單個(gè)Web服務(wù)提供的功能有限，有必要將多個(gè)服務(wù)組裝成一個(gè)價(jià)值增值的、粒度更大的服務(wù)或系統(tǒng)以滿足復(fù)雜的應(yīng)用需求。但在服務(wù)組合過程中，因存在接口類型、數(shù)據(jù)格式或交互協(xié)議不一致等失配情況，導(dǎo)致服務(wù)無法正確組合。服務(wù)失配檢測(cè)可準(zhǔn)確捕捉失配點(diǎn)，為實(shí)現(xiàn)服務(wù)的正確組合奠定基礎(chǔ)。
　　 從互操作性

2、分層的角度分析，服務(wù)失配可能發(fā)生在簽名、行為、語(yǔ)義等層次。其中行為層的失配研究是關(guān)鍵也是難點(diǎn)，本文研究Web服務(wù)在行為層次的失配。如果參與交互的服務(wù)最終能到達(dá)各自的終止?fàn)顟B(tài)，則服務(wù)交互過程不存在失配，否則就存在失配。換言之，本文將服務(wù)的失配檢測(cè)問題轉(zhuǎn)化為服務(wù)兼容性判定問題。
　　 形式化驗(yàn)證技術(shù)(如模型檢測(cè))作為軟件質(zhì)量保證的一種重要方法，目前已廣泛應(yīng)用于Web服務(wù)相關(guān)性質(zhì)驗(yàn)證。限界模型檢測(cè)(BMC)采用由局部到全局漸進(jìn)式檢測(cè)，

3、能快速尋找到反例。本文采用BMC圍繞Web服務(wù)失配檢測(cè)展開了研究，具體內(nèi)容包括：(1)提出了一種基于NuSMV的Web服務(wù)失配檢測(cè)方法。首先給出Web服務(wù)交互行為以及兼容性質(zhì)的形式化描述，然后利用支持BMC的模型檢測(cè)工具NuSMV驗(yàn)證服務(wù)交互模型是否滿足兼容性質(zhì)，性質(zhì)不滿足時(shí)，給出反例說明。(2)提出了一種基于SMT的Web服務(wù)失配檢測(cè)方法，通過檢測(cè)服務(wù)交互過程死鎖狀態(tài)是否可達(dá)來判定Web服務(wù)交互行為的兼容性。首先對(duì)Web服務(wù)交互行為進(jìn)