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

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

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