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

1、面向服務(wù)的體系結(jié)構(gòu)的出現(xiàn)和發(fā)展使得Web服務(wù)成為當(dāng)今服務(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)

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

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

4、　(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)形成一