Web組合服務的建模與驗證.pdf

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

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

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