基于條件轉(zhuǎn)移的模型檢測研究及在Web服務(wù)驗證中的應(yīng)用.pdf

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

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

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