基于擴(kuò)展確定有限自動(dòng)機(jī)的Web服務(wù)自動(dòng)組合與形式化驗(yàn)證.pdf

1、Web服務(wù)組合可以有效地支持企業(yè)內(nèi)部跨部門的橫向業(yè)務(wù)集成，以及橫跨業(yè)務(wù)伙伴的企業(yè)間業(yè)務(wù)集成。組合Web服務(wù)驗(yàn)證可以檢查集成業(yè)務(wù)是否是可終止的、有效的和正確的。兩者蘊(yùn)藏著巨大的商業(yè)價(jià)值。本文從分析Web服務(wù)的非形式化描述開(kāi)始，對(duì)Web服務(wù)建模、Web服務(wù)自動(dòng)選擇、Web服務(wù)自動(dòng)組合和組合Web服務(wù)形式化驗(yàn)證中的關(guān)鍵問(wèn)題，進(jìn)行了深入研究。 首先，根據(jù)Web服務(wù)與用戶交互的特點(diǎn)，提出擴(kuò)展確定有限自動(dòng)機(jī)EDFA，用來(lái)準(zhǔn)確地描述Web服務(wù)

2、：EDFA的狀態(tài)描述Web服務(wù)在與用戶交互的過(guò)程中維護(hù)的狀態(tài)；EDFA的狀態(tài)轉(zhuǎn)移及其標(biāo)注描述Web服務(wù)與用戶之間的消息交換。由EDFA可以得到Web服務(wù)與用戶交互過(guò)程中所有的消息交換序列。 其次，提出基于EDFA的Web服務(wù)形式化模型{Ps，rs，ls}。P,是一個(gè)EDFA，用來(lái)描述服務(wù)與其用戶交互的過(guò)程，刻畫出對(duì)外公布的Web服務(wù)的外部行為；rs也是一個(gè)EDFA，用來(lái)描述服務(wù)以用戶的角色與不同Web服務(wù)交互的過(guò)程，刻畫出無(wú)需對(duì)

3、外公布的Web服務(wù)的內(nèi)部行為；ls是一個(gè)Web服務(wù)和原子過(guò)程的對(duì)照表，說(shuō)明服務(wù)的每個(gè)執(zhí)行步驟與其調(diào)用的服務(wù)的對(duì)應(yīng)關(guān)系。 然后，給出將OWL-S過(guò)程模型轉(zhuǎn)換為EDFA的方法：先使用EDFA表示原子過(guò)程；針對(duì)OWL-S過(guò)程模型中的九種控制結(jié)構(gòu)給出基于EDFA的過(guò)程組合規(guī)則；再使用過(guò)程組合規(guī)則將表示原子過(guò)程的EDFA進(jìn)行連接，從而得到表示組合過(guò)程的EDFA，完成OWL-S過(guò)程模型到EDFA的轉(zhuǎn)換。 最后，在擴(kuò)展確定有限自動(dòng)機(jī)E

4、DFA的基礎(chǔ)上完成三項(xiàng)工作： 第一，提出基于Web服務(wù)行為的語(yǔ)義匹配方法，用來(lái)在開(kāi)放的網(wǎng)絡(luò)環(huán)境下自動(dòng)準(zhǔn)確地選出符合用戶需求的Web服務(wù)； 第二，提出一個(gè)受限的描述邏輯Tableau算法，結(jié)合基于EDFA的過(guò)程組合規(guī)則，在開(kāi)放的網(wǎng)絡(luò)環(huán)境下實(shí)現(xiàn)Web服務(wù)自動(dòng)組合，并給出獲得組合Web服務(wù)形式化模型的方法； 第三，在組合Web服務(wù)形式化模型的基礎(chǔ)上，給出一系列形式化判定方法，完成組合Web服務(wù)功能和組合Web服務(wù)運(yùn)行過(guò)