基于多智能体系统模型检测与抽象技术的Web服务组合验证

发布时间：2018-04-22 06:02

本文选题：Web服务组合验证 + 多智能体系统模型检测　；参考：《华侨大学》2014年硕士论文

【摘要】：面向服务的体系结构的出现和发展使得Web服务成为当今服务及软件开发的发展趋势。由于功能有限的单一的Web服务在多数情况下不能满足用户的需求，出现了将多种web服务按某种特定的组合集成一个面向具有不同需求用户的有统一接口的服务的技术。然而，服务组合的可信性质受到了来自于服务本身或者其运行环境各个因素的威胁。针对服务的可信性质，研究者们在不断地寻求对验证web服务组合的方法。目前验证Web服务组合方法多是形式化方法。相对于传统的形式化方法，模型检测的优点是验证的全自动化和验证所给出的证据和反例。其另一个不太易见的优点是，它不需要在验证所涉及逻辑的全体论域中推理待验证公式是否成立，而只需将待检测系统的形式化模型作为论域。在众多用模型检测检验Web服务组合性质的技术中，多智能体系统模型检测的优势在于，它不但能验证时态公式，还能验证认知公式。状态爆炸问题是模型检测面临的主要的问题之一，，也当在模型检测多智能体系统的主要瓶颈之列。抽象作为解决状态爆炸问题的一种优化手段，受到了许多研究者的青睐，其研究成果也不断出现。本文探索一种多智能体系统模型检测图状反例向导的抽象，并将之应用于Web服务组合验证中，这是任何以往的Web服务组合验证工作都没有做到的。另外，以往的反例向导的抽象或者未针对多智能体系统，或者所用形式化模型的形式化程度较本文的Kripke结构形式化程度低。本文的方法论在文中获得了数学上严格证明。并且，通过实验证明了该方法论在性能上的优越性。论文的主要研究工作概括如下：（1）提出多智能体系统的Kripke结构，提出并证明了其抽象模型和一种获得初始抽象系统的近似方法。（2）提出了多智能体系统模型检测的一种图状反例，给出并证明了图状反例的某些性质。（3）提出一种图状反例向导的多智能体系统模型检测抽象精化方法。（4）根据我们的分析，Web服务组合中常用的规范是BPEL。采用了以往的将BPEL描述的Web服务组合业务流程转化多智能体系统的一种方法。（5）形成一个基于多智能体系统模型检测及其图状反例向导的抽象与精化技术的Web服务组合验证方法论。
[Abstract]:With the emergence and development of Service-Oriented Architecture, Web Services has become the trend of service and software development. Because a single Web service with limited functions can not meet the needs of users in most cases, a technology has emerged to integrate multiple web services into a uniform interface for users with different requirements according to a particular composition. However, the trustworthiness of service composition is threatened by various factors from the service itself or its running environment. In view of the trusted nature of services, researchers are constantly looking for ways to verify the composition of web services. At present, Web service composition methods are mostly formal. Compared with the traditional formal methods, the advantages of model checking are the full automation of verification and the evidence and counterexample given by verification. Another less visible advantage is that it does not need to infer whether the formula to be verified is valid in the whole domain of the logic involved, but only takes the formal model of the system to be detected as a domain. Among the many techniques used to test the properties of Web services composition, the advantage of model checking in multi-agent system is that it not only verifies temporal formula, but also verifies cognitive formula. The problem of state explosion is one of the main problems in model detection, and it is also one of the main bottlenecks in multi-agent system. Abstract, as an optimization method to solve the state explosion problem, has been favored by many researchers, and its research results are also emerging. This paper explores the abstraction of a multi-agent model checking diagram counterexample wizard and applies it to Web service composition verification, which has not been done in any previous Web service composition verification work. In addition, the former counterexample wizards are either abstract or not specific to multi-agent systems, or the formalization of the formal model used is lower than the formalization of the Kripke structure in this paper. The methodology of this paper is proved mathematically. Moreover, the superiority of the methodology in performance has been proved by experiments. The main research work of the thesis is summarized as follows: 1) the Kripke structure of the multi-agent system is proposed, and its abstract model and an approximate method to obtain the initial abstract system are presented and proved. In this paper, a graph counterexample for model checking of multi-agent system is presented, and some properties of graph counterexample are given and proved. This paper presents an abstract refinement method for multi-agent system model detection based on graphical counterexample guide. According to our analysis, the common specification in Web service composition is BPEL. This paper adopts a method of transforming Web services composition business process described by BPEL into multi agent system. A methodology of Web service composition verification based on multi-agent system model checking and its schematic counterexample wizard is formed.
【学位授予单位】：华侨大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP393.09

【参考文献】