【摘要】：Web服務(wù)是一種面向服務(wù)計(jì)算的應(yīng)用。不同的開發(fā)商通過使用不同的邏輯控制流將異構(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ǔ)�；跅l件轉(zhuǎn)移的模型檢測(cè)方法分為基于動(dòng)態(tài)建模方法的動(dòng)態(tài)檢測(cè)方法和基于靜態(tài)建模方法的靜態(tài)檢測(cè)方法�；跅l件轉(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è)過程中始終存在的問題,對(duì)于大規(guī)模的Web組合服務(wù),狀態(tài)爆炸問題依然存在,本文采用基于外存的條件轉(zhuǎn)移模型檢測(cè)方法解決該問題。本文結(jié)合寬度優(yōu)先搜索算法和基于外存的思想提出了基于外存的條件轉(zhuǎn)移模型檢測(cè)算法,該算法使用條件轉(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)證更大規(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é)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TP393.09

【參考文獻(xiàn)】

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

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

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

3 劉峰;陳笑蓉;;基于π演算的工作流模型檢驗(yàn)[J];計(jì)算機(jī)工程;2011年23期

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

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

，

本文編號(hào)：2495781