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

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

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

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