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

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

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

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