基于LSC的Web服務(wù)組合模型驗(yàn)證方法研究.pdf

1、隨著Web服務(wù)技術(shù)的迅速發(fā)展,越來越多的Web服務(wù)運(yùn)行在Internet上,這些單一的Web服務(wù)功能有限,不能滿足用戶的需求,但是這些單個(gè)、基本的Web服務(wù),允許其他應(yīng)用程序通過互聯(lián)網(wǎng)連接及調(diào)用,組裝成更復(fù)雜的應(yīng)用以便用于表達(dá)業(yè)務(wù)流程。因此,如何確保組合起來的Web服務(wù)的正確性,成為Web服務(wù)研究領(lǐng)域中的熱點(diǎn)。形式化方法在對(duì)基于消息通信和并發(fā)系統(tǒng)建模和分析方面已經(jīng)成為非常重要的手段,其中模型檢測作為一種自動(dòng)驗(yàn)證技術(shù)被許多學(xué)者應(yīng)用于Web

2、服務(wù)組合的驗(yàn)證。
　　 本文首先介紹了模型檢測和時(shí)態(tài)邏輯的基本概念及業(yè)務(wù)流程執(zhí)行語言(BPEL)和時(shí)間自動(dòng)機(jī)的相關(guān)知識(shí),并基于模型檢測方法對(duì)Web服務(wù)組合驗(yàn)證開展研究,完成的主要工作如下：⑴在分析LSC的語法和基于路徑的語義基礎(chǔ)上,改進(jìn)了LSC圖到時(shí)態(tài)邏輯公式的轉(zhuǎn)換方法,得到較短的時(shí)態(tài)邏輯公式,以便降低傳統(tǒng)的模型檢測對(duì)Web服務(wù)組合進(jìn)行驗(yàn)證的復(fù)雜性。⑵提出了一種基于LSC的Web服務(wù)組合驗(yàn)證方法。該方法首先擴(kuò)展了WS-BPEL的

3、時(shí)間屬性,并給出了BPEL描述的業(yè)務(wù)流程到時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)轉(zhuǎn)化方法;其次,對(duì)LSC語法及語義進(jìn)行時(shí)間屬性方面的擴(kuò)展,Web服務(wù)組合需要滿足的場景用擴(kuò)展后的LSC圖來描述,并將LSC圖轉(zhuǎn)換為觀察時(shí)間自動(dòng)機(jī);最后,通過將觀察時(shí)間自動(dòng)機(jī)與BPEL轉(zhuǎn)化來的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)同時(shí)嵌入到模型檢測工具UPPAAL中,完成BPEL描述的業(yè)務(wù)流程是否滿足LSC表示的性質(zhì)的檢測。⑶通過一個(gè)實(shí)例并使用UPPAAL工具對(duì)轉(zhuǎn)換后的Web服務(wù)組合和場景性質(zhì)進(jìn)行驗(yàn)證。實(shí)例