基于時(shí)間自動(dòng)機(jī)的Web服務(wù)模型檢測(cè).pdf

1、Web服務(wù)技術(shù)給企業(yè)的應(yīng)用程序集成帶來了方便,但是分布的單個(gè)Web服務(wù)功能簡(jiǎn)單有限,因此有必要將它們進(jìn)行組合。Web服務(wù)的這種組合方式使得各原子服務(wù)間產(chǎn)生了大量復(fù)雜的信息交互。為了保障組合Web服務(wù)的正確性,有必要對(duì)其運(yùn)行過程進(jìn)行檢測(cè)。模型檢測(cè)技術(shù)以其自動(dòng)化程度高,在Web服務(wù)的形式化驗(yàn)證中倍受關(guān)注。
　　傳統(tǒng)的模型檢測(cè)方法不能保證帶有嚴(yán)格時(shí)間約束的實(shí)時(shí)組合Web服務(wù)的正確性。本文將帶有時(shí)間約束的組合Web服務(wù)建模為一組時(shí)間自動(dòng)機(jī)

2、,并用基于時(shí)間自動(dòng)機(jī)的模型檢測(cè)工具驗(yàn)證了組合Web服務(wù)實(shí)時(shí)的時(shí)態(tài)邏輯特性、組合Web服務(wù)中存在的特征沖突問題及組合Web服務(wù)的時(shí)態(tài)認(rèn)知邏輯特性。為了系統(tǒng)的研究組合Web服務(wù),還提出了一種執(zhí)行代價(jià)較小的Web服務(wù)組合方法。本文的工作主要體現(xiàn)在以下幾個(gè)方面:
　　(1)提出了用基于時(shí)間自動(dòng)機(jī)的模型檢測(cè)技術(shù)對(duì)組合Web服務(wù)進(jìn)行形式化驗(yàn)證的方法。將組合Web服務(wù)建模成一組相互通信的時(shí)間自動(dòng)機(jī),并用UPPAAL模擬其運(yùn)行過程,驗(yàn)證其系統(tǒng)的一

3、些實(shí)時(shí)時(shí)態(tài)邏輯特性。以兩個(gè)組合Web服務(wù)為例闡述了該驗(yàn)證過程,并發(fā)現(xiàn)其中一個(gè)服務(wù)存在死鎖問題;通過分析死鎖產(chǎn)生的路徑完善了該服務(wù)的協(xié)議,從而消除了死鎖。此外,首次采用該技術(shù)對(duì)組合Web服務(wù)的特征沖突問題進(jìn)行了分析和檢測(cè)。發(fā)現(xiàn)了在線股票交易系統(tǒng)的特征沖突現(xiàn)象,驗(yàn)證了該服務(wù)的特征沖突屬性。
　　(2)提出了用基于Verics的有界模型檢測(cè)技術(shù)對(duì)組合Web服務(wù)系統(tǒng)的時(shí)態(tài)認(rèn)知邏輯特性進(jìn)行驗(yàn)證。將組合Web服務(wù)建模成時(shí)間自動(dòng)機(jī),用模型檢測(cè)工