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

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

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

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