基于時間自動機的Web服務(wù)模型檢測.pdf

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

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

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