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

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

【參考文獻(xiàn)】

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

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

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

本文編號(hào)：1785895