基于多智能體系統(tǒng)模型檢測與抽象技術的Web服務組合驗證.pdf

1、面向服務的體系結構的出現(xiàn)和發(fā)展使得Web服務成為當今服務及軟件開發(fā)的發(fā)展趨勢。由于功能有限的單一的Web服務在多數(shù)情況下不能滿足用戶的需求,出現(xiàn)了將多種 web服務按某種特定的組合集成一個面向具有不同需求用戶的有統(tǒng)一接口的服務的技術。然而,服務組合的可信性質受到了來自于服務本身或者其運行環(huán)境各個因素的威脅。針對服務的可信性質,研究者們在不斷地尋求對驗證web服務組合的方法。
　　目前驗證Web服務組合方法多是形式化方法。相對于傳統(tǒng)

2、的形式化方法,模型檢測的優(yōu)點是驗證的全自動化和驗證所給出的證據和反例。其另一個不太易見的優(yōu)點是,它不需要在驗證所涉及邏輯的全體論域中推理待驗證公式是否成立,而只需將待檢測系統(tǒng)的形式化模型作為論域。在眾多用模型檢測檢驗Web服務組合性質的技術中,多智能體系統(tǒng)模型檢測的優(yōu)勢在于,它不但能驗證時態(tài)公式,還能驗證認知公式。狀態(tài)爆炸問題是模型檢測面臨的主要的問題之一,也當在模型檢測多智能體系統(tǒng)的主要瓶頸之列。抽象作為解決狀態(tài)爆炸問題的一種優(yōu)化手段

3、,受到了許多研究者的青睞,其研究成果也不斷出現(xiàn)。
　　本文探索一種多智能體系統(tǒng)模型檢測圖狀反例向導的抽象,并將之應用于Web服務組合驗證中,這是任何以往的Web服務組合驗證工作都沒有做到的。另外,以往的反例向導的抽象或者未針對多智能體系統(tǒng),或者所用形式化模型的形式化程度較本文的 Kripke結構形式化程度低。本文的方法論在文中獲得了數(shù)學上嚴格證明。并且,通過實驗證明了該方法論在性能上的優(yōu)越性。論文的主要研究工作概括如下:
　

4、　(1)提出多智能體系統(tǒng)的Kripke結構,提出并證明了其抽象模型和一種獲得初始抽象系統(tǒng)的近似方法。
　　(2)提出了多智能體系統(tǒng)模型檢測的一種圖狀反例,給出并證明了圖狀反例的某些性質。
　　(3)提出一種圖狀反例向導的多智能體系統(tǒng)模型檢測抽象精化方法。
　　(4)根據我們的分析,Web服務組合中常用的規(guī)范是BPEL。采用了以往的將BPEL描述的Web服務組合業(yè)務流程轉化多智能體系統(tǒng)的一種方法。
　　(5)形成一