一種Web服務(wù)組合的自動化模型檢測方法.pdf

1、如今 Web服務(wù)廣泛分布于互聯(lián)網(wǎng)中,它們通過彼此之間的交互實(shí)現(xiàn)對問題的協(xié)作求解。然而,在交互過程中,一些非預(yù)期、“不正?！钡男畔⒔换r(shí)有發(fā)生,嚴(yán)重影響了系統(tǒng)的質(zhì)量及健壯性,有可能使用戶得不到正確結(jié)果。因此,模型檢測 Web服務(wù)組合的時(shí)態(tài)認(rèn)知性質(zhì),保障 Web服務(wù)的正確運(yùn)行就成為了模型檢測領(lǐng)域的熱門研究方向。目前,國內(nèi)外針對 Web服務(wù)組合的形式化驗(yàn)證正處于起步階段,整個驗(yàn)證過程的自動化程度很低,各個技術(shù)環(huán)節(jié)都需要大量的人工操作。為了提高

2、 Web服務(wù)流程驗(yàn)證的自動化程度,本文提出將Web服務(wù)組合的BPEL流程自動轉(zhuǎn)化為模型檢測工具M(jìn)CTK輸入代碼的一系列轉(zhuǎn)換算法。最后利用這些算法在MCTK環(huán)境下對VTA協(xié)議和STS協(xié)議進(jìn)行了形式化驗(yàn)證,并自動構(gòu)建了貸款服務(wù)協(xié)議的狀態(tài)轉(zhuǎn)換圖。取得的研究成果有:
　　(1)針對Web服務(wù)描述語言BPEL,給出相關(guān)活動語義。引入遷移七元組概念,基于活動語義,建立BPEL活動與能夠反映系統(tǒng)狀態(tài)遷移關(guān)系的遷移七元組的一一對應(yīng),為實(shí)現(xiàn)流程的自

3、動化驗(yàn)證打下基礎(chǔ);
　　(2)分別提出將BPEL控制流、數(shù)據(jù)流轉(zhuǎn)化為遷移七元組集合的轉(zhuǎn)換算法B2T和F2T。這些算法自動將BPEL流程轉(zhuǎn)化為遷移七元組集合,實(shí)現(xiàn)了將組合業(yè)務(wù)流程自動轉(zhuǎn)化為多分支狀態(tài)轉(zhuǎn)換圖的功能;
　　(3)提出根據(jù)遷移七元組集合自動生成MCTK代碼的轉(zhuǎn)換算法T2M。為了實(shí)現(xiàn)控制流的全自動檢測,T2M算法根據(jù)遷移七元組集合中各元組的相互關(guān)系,結(jié)合MCTK語言自身特點(diǎn),自動生成用來描述流程的MCTK代碼,避免了繁