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

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

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

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