【摘要】：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ǔ)。基于條件轉(zhuǎn)移的模型檢測方法分為基于動態(tài)建模方法的動態(tài)檢測方法和基于靜態(tài)建模方法的靜態(tài)檢測方法�；跅l件轉(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)移模型檢測算法,該算法使用條件轉(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)移的模型檢測方法具有驗證更大規(guī)模Web組合服務(wù)安全性的能力。
[Abstract]:Web service is a service-oriented computing application. Different developers combine heterogeneous and multi-platform Web services into a new Web service by using different logical control flows, which is called Web composite service. The security of web composite service control flow is difficult to guarantee. The purpose of this paper is to solve the security of Web composite service control flow. In this paper, Web composite service is regarded as a multi-agent system, and the model detection method based on conditional transfer is used to verify the Web composite service. This model detection method is based on the construction of conditional transfer system. The model detection method based on conditional transfer is divided into dynamic detection method based on dynamic modeling method and static detection method based on static modeling method. The core idea of conditional transfer model detection method is to generate the state set and transition relation set of the system according to the rule set. The dynamic detection method has good advantages in modeling efficiency and error location efficiency. In this paper, the dynamic detection method is used to verify the Web composite service. State explosion is always a problem in the process of model detection. For large-scale Web composite services, the problem of state explosion still exists. In this paper, the conditional transition model detection method based on external memory is used to solve this problem. In this paper, a conditional transfer model detection algorithm based on external memory is proposed based on the idea of width first search and external memory. The algorithm uses the idea of conditional transfer model detection method and blocks a large number of newly generated states. This method relieves the pressure of memory and makes it possible for the model detector to verify the large-scale system. In this paper, the rule set of Web composite service and the conditional transfer system of Web composite service generated according to the rule set are given, and the counterexample path of Web composite service is analyzed. In this paper, the model detector NuSMV is improved and the improved model detector is used to verify the Web composite service, and then compared with other model detector (Spin,NuSMV, etc.). It is concluded that the model detection method based on conditional transfer has the ability to verify the security of larger Web composite services.
【學(xué)位授予單位】：電子科技大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：TP393.09

【參考文獻】

相關(guān)期刊論文 前5條

1 程道雷;肖美華;劉欣倩;梅映天;李偉;;運用SPIN對開放授權(quán)協(xié)議OAuth 2.0的分析與驗證[J];計算機工程與科學(xué);2015年11期

2 劉博;李蜀瑜;;基于NuSMV的AADL行為模型驗證的探究[J];計算機技術(shù)與發(fā)展;2012年02期

3 劉峰;陳笑蓉;;基于π演算的工作流模型檢驗[J];計算機工程;2011年23期

4 張國鋒;何俊;徐從富;;一種基于BPEL的通用安全控制模塊設(shè)計方法[J];計算機應(yīng)用;2008年11期

5 黎升洪;繆淮扣;張新林;;線性時態(tài)邏輯中的特性模式[J];計算機應(yīng)用;2006年08期

，

本文編號：2495781