本文選題：Web服務組合驗證 + 多智能體系統(tǒng)模型檢測��； 參考：《華僑大學》2014年碩士論文

【摘要】：面向服務的體系結構的出現(xiàn)和發(fā)展使得Web服務成為當今服務及軟件開發(fā)的發(fā)展趨勢。由于功能有限的單一的Web服務在多數(shù)情況下不能滿足用戶的需求，出現(xiàn)了將多種web服務按某種特定的組合集成一個面向具有不同需求用戶的有統(tǒng)一接口的服務的技術。然而，服務組合的可信性質受到了來自于服務本身或者其運行環(huán)境各個因素的威脅。針對服務的可信性質，研究者們在不斷地尋求對驗證web服務組合的方法。 目前驗證Web服務組合方法多是形式化方法。相對于傳統(tǒng)的形式化方法，模型檢測的優(yōu)點是驗證的全自動化和驗證所給出的證據和反例。其另一個不太易見的優(yōu)點是，它不需要在驗證所涉及邏輯的全體論域中推理待驗證公式是否成立，而只需將待檢測系統(tǒng)的形式化模型作為論域。在眾多用模型檢測檢驗Web服務組合性質的技術中，多智能體系統(tǒng)模型檢測的優(yōu)勢在于，它不但能驗證時態(tài)公式，還能驗證認知公式。狀態(tài)爆炸問題是模型檢測面臨的主要的問題之一，，也當在模型檢測多智能體系統(tǒng)的主要瓶頸之列。抽象作為解決狀態(tài)爆炸問題的一種優(yōu)化手段，受到了許多研究者的青睞，其研究成果也不斷出現(xiàn)。 本文探索一種多智能體系統(tǒng)模型檢測圖狀反例向導的抽象，并將之應用于Web服務組合驗證中，這是任何以往的Web服務組合驗證工作都沒有做到的。另外，以往的反例向導的抽象或者未針對多智能體系統(tǒng)，或者所用形式化模型的形式化程度較本文的Kripke結構形式化程度低。本文的方法論在文中獲得了數(shù)學上嚴格證明。并且，通過實驗證明了該方法論在性能上的優(yōu)越性。論文的主要研究工作概括如下： （1）提出多智能體系統(tǒng)的Kripke結構，提出并證明了其抽象模型和一種獲得初始抽象系統(tǒng)的近似方法。 （2）提出了多智能體系統(tǒng)模型檢測的一種圖狀反例，給出并證明了圖狀反例的某些性質。 （3）提出一種圖狀反例向導的多智能體系統(tǒng)模型檢測抽象精化方法。 （4）根據我們的分析，Web服務組合中常用的規(guī)范是BPEL。采用了以往的將BPEL描述的Web服務組合業(yè)務流程轉化多智能體系統(tǒng)的一種方法。 （5）形成一個基于多智能體系統(tǒng)模型檢測及其圖狀反例向導的抽象與精化技術的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

【參考文獻】

相關期刊論文 前2條

1 駱翔宇;陳艷;;Web服務的形式化驗證[J];計算機工程;2010年05期

2 駱翔宇;王昆;王鳳釵;;一種Web服務組合的認知模型檢測方法[J];小型微型計算機系統(tǒng);2011年10期

本文編號：1785895