1、Web組合服務(wù)是一種基于面向服務(wù)的應(yīng)用程序,它可以將多個異構(gòu)的、跨平臺的,不同開發(fā)者所開發(fā)Web應(yīng)用程序加以組合,利用不同的邏輯控制流跳轉(zhuǎn),組成功能不一樣的基于互聯(lián)網(wǎng)的應(yīng)用程序。在它產(chǎn)生以來,就引起了業(yè)界廣泛的關(guān)注。而大規(guī)模的Web組合服務(wù)中由了很多異構(gòu)的Web服務(wù)組成,它的控制流程很難得到保證,故本文利用模型檢測的方法來驗證大規(guī)模Web組合服務(wù)的系統(tǒng)安全性、可用性和驗證其多主體認(rèn)知邏輯。
　　本文首先對相關(guān)的技術(shù)和基礎(chǔ)知識做了介

2、紹,并對當(dāng)前學(xué)界對Web服務(wù)的模型檢測驗證研究現(xiàn)狀進(jìn)行了總結(jié)。接著本文將Web組合服務(wù)看做一個帶有多主體的認(rèn)知邏輯系統(tǒng),并證明其可行性,給出BPEL語言中的活動的遷移元組。接著本文為了增強(qiáng)模型檢測算法對于大規(guī)模系統(tǒng)的把控能力,更好地解決由于系統(tǒng)空間狀態(tài)爆炸而產(chǎn)生的問題,引入了磁盤Mysql數(shù)據(jù)庫對系統(tǒng)狀態(tài)進(jìn)行管理。通過對寬度優(yōu)先狀態(tài)搜索算法中,利用數(shù)據(jù)庫減少每層計算機(jī)系統(tǒng)需要處理的模型系統(tǒng)狀態(tài)。并且利用哈希算法,盡量減少算法的IO讀取次

3、數(shù),在可接受的系統(tǒng)資源消耗的情況下,達(dá)到系統(tǒng)全空間狀態(tài)搜索的目的,并返回系統(tǒng)所有可能的反例。最后本文根據(jù)日常生活中,電子商務(wù)的場景,構(gòu)建出電子商務(wù)的交易模型,給出其Promela語言形式,并給出此模型的多主體認(rèn)知邏輯到LTL的轉(zhuǎn)化。并利于本論文提出算法的實現(xiàn)的模型檢測器對交易模型的檢測結(jié)果,與其他模型檢測器(如Spin等)的檢測結(jié)果作比較。
　　本文從建模和算法實現(xiàn)的兩方面入手,提出一種可以對大規(guī)模Web組合服務(wù)進(jìn)行模型檢測驗證,