基于條件轉移的模型檢測研究及在Web服務驗證中的應用.pdf

1、Web服務是一種面向服務計算的應用。不同的開發(fā)商通過使用不同的邏輯控制流將異構、多平臺的Web服務組合成一個新的Web服務，稱之為Web組合服務。Web組合服務控制流的安全性很難得到保障，本文的目的就是解決Web組合服務控制流的安全性。
　　本文把Web組合服務看作是多主體系統(tǒng)，使用基于條件轉移的模型檢測方法對Web組合服務驗證，這種模型檢測方法以構建條件轉移系統(tǒng)為基礎。基于條件轉移的模型檢測方法分為基于動態(tài)建模方法的動態(tài)檢測方法

2、和基于靜態(tài)建模方法的靜態(tài)檢測方法。基于條件轉移模型檢測方法的核心思想是根據(jù)規(guī)則集產(chǎn)生系統(tǒng)的狀態(tài)集以及轉移關系集合，動態(tài)檢測方法在建模效率以及錯誤定位效率方面有很好的優(yōu)越性，本文采用動態(tài)檢測方法對Web組合服務驗證。狀態(tài)爆炸是模型檢測過程中始終存在的問題，對于大規(guī)模的Web組合服務，狀態(tài)爆炸問題依然存在，本文采用基于外存的條件轉移模型檢測方法解決該問題。本文結合寬度優(yōu)先搜索算法和基于外存的思想提出了基于外存的條件轉移模型檢測算法，該算法使

3、用條件轉移模型檢測方法的思想并對新產(chǎn)生的一層數(shù)量巨大的狀態(tài)進行分塊操作，該方法緩解了內(nèi)存的壓力，使得模型檢測器驗證大規(guī)模的系統(tǒng)成為了可能。本文給出了Web組合服務的規(guī)則集和根據(jù)規(guī)則集產(chǎn)生的Web組合服務的條件轉移系統(tǒng)，并對Web組合服務的反例路徑進行分析。
　　本文改進模型檢測器NuSMV并使用改進的模型檢測器對Web組合服務驗證，然后與其它的模型檢測器（Spin，NuSMV等）進行實驗對比，得出基于條件轉移的模型檢測方法具有驗證