一種基于Mealy機(jī)的BPEL程序驗(yàn)證模型研究.pdf

1、BPEL作為描述Web服務(wù)編制的語(yǔ)言之一，在商業(yè)流程中被用來(lái)描述活動(dòng)和對(duì)活動(dòng)的控制。BPEL具有類似程序設(shè)計(jì)語(yǔ)言的語(yǔ)法結(jié)構(gòu)，如順序、分支和循環(huán)等，能表達(dá)對(duì)業(yè)務(wù)流程的控制。BPEL語(yǔ)法中還有專為商業(yè)流程設(shè)計(jì)的結(jié)構(gòu)，兼顧了IT和商業(yè)兩個(gè)領(lǐng)域的需求。但是這給BPEL程序驗(yàn)證帶來(lái)了難題。BPEL不是一種可執(zhí)行的程序語(yǔ)言，往往冗長(zhǎng)而復(fù)雜，仍然存在二義性、不一致性和不完備性。為了提高Web服務(wù)中BPEL應(yīng)用程序的健壯性，有必要改進(jìn)程序驗(yàn)證的方法。

2、 本文對(duì)現(xiàn)有基于模型檢測(cè)技術(shù)的BPEL程序驗(yàn)證方法進(jìn)行了研究，提出了一種基于Mealy機(jī)的驗(yàn)證模型BVM(BPEL Verification Machine)，并利用該模型建立了一個(gè)驗(yàn)證BPEL程序性質(zhì)的方法。本文通過(guò)已知BPEL程序源碼找出驗(yàn)證程序需要的BVM模型M和通過(guò)用戶需求說(shuō)明書(shū)找出待驗(yàn)證的性質(zhì)P，設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)在模型檢測(cè)器NuSMV中驗(yàn)證M是否滿足P的引擎。實(shí)驗(yàn)顯示該方法能夠驗(yàn)證包括補(bǔ)償?shù)腂PEL程序，彌補(bǔ)了現(xiàn)有方法在