基于条件转移的模型检测研究及在Web服务验证中的应用

发布时间：2019-06-09 18:22

【摘要】：Web服务是一种面向服务计算的应用。不同的开发商通过使用不同的逻辑控制流将异构、多平台的Web服务组合成一个新的Web服务,称之为Web组合服务。Web组合服务控制流的安全性很难得到保障,本文的目的就是解决Web组合服务控制流的安全性。本文把Web组合服务看作是多主体系统,使用基于条件转移的模型检测方法对Web组合服务验证,这种模型检测方法以构建条件转移系统为基础。基于条件转移的模型检测方法分为基于动态建模方法的动态检测方法和基于静态建模方法的静态检测方法。基于条件转移模型检测方法的核心思想是根据规则集产生系统的状态集以及转移关系集合,动态检测方法在建模效率以及错误定位效率方面有很好的优越性,本文采用动态检测方法对Web组合服务验证。状态爆炸是模型检测过程中始终存在的问题,对于大规模的Web组合服务,状态爆炸问题依然存在,本文采用基于外存的条件转移模型检测方法解决该问题。本文结合宽度优先搜索算法和基于外存的思想提出了基于外存的条件转移模型检测算法,该算法使用条件转移模型检测方法的思想并对新产生的一层数量巨大的状态进行分块操作,该方法缓解了内存的压力,使得模型检测器验证大规模的系统成为了可能。本文给出了Web组合服务的规则集和根据规则集产生的Web组合服务的条件转移系统,并对Web组合服务的反例路径进行分析。本文改进模型检测器NuSMV并使用改进的模型检测器对Web组合服务验证,然后与其它的模型检测器(Spin,NuSMV等)进行实验对比,得出基于条件转移的模型检测方法具有验证更大规模Web组合服务安全性的能力。
[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.
【学位授予单位】：电子科技大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP393.09

【参考文献】