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

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

【參考文獻】

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

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

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

本文編號：1785895