基于π-演算的WS-BPEL建模與實(shí)現(xiàn).pdf

1、業(yè)務(wù)流程的設(shè)計(jì)和驗(yàn)證是所有工作流產(chǎn)品的一個(gè)主要功能。為了能夠盡早發(fā)現(xiàn)流程建模中死鎖、缺少同步等問題，大部分工作流產(chǎn)品都需要提供基于形式化分析和建模的功能。由于WS—BPEL(Web Services Business Process Execution Language)描述業(yè)務(wù)流程是半形式化的，不易檢測(cè)與驗(yàn)證，也沒有相應(yīng)形式化工具支持，這使得Web服務(wù)組合的正確性難以保證，其業(yè)務(wù)流程也無法在較抽象的層次上進(jìn)行跟蹤。 本文結(jié)合實(shí)

2、驗(yàn)室承擔(dān)的國家863科研攻關(guān)項(xiàng)目，針對(duì)業(yè)務(wù)流程內(nèi)部邏輯的正確性問題展開研究，探索利用進(jìn)程代數(shù)π—演算作為形式化工具，對(duì)WS—BPEL描述的業(yè)務(wù)流程進(jìn)行建模和驗(yàn)證。主要進(jìn)行的工作如下： 1．本文提出了業(yè)務(wù)流程建模與驗(yàn)證的體系結(jié)構(gòu)BPMV(Business Process Modeling andVerfication)、說明了本文要解決問題及所采取的步驟，分析了基于Petri網(wǎng)、自動(dòng)機(jī)理論、進(jìn)程代數(shù)對(duì)WS—BPEL活動(dòng)進(jìn)行建模的方

3、法和成果。 2．本文分析了國內(nèi)外基于π—演算對(duì)WS—BPEL活動(dòng)建模的相關(guān)研究現(xiàn)狀。說明了π—演算適合對(duì)WS—BPEL活動(dòng)進(jìn)行建模的原因，完善了π—演算對(duì)WS—BPEL活動(dòng)的建模，在此基礎(chǔ)上給出了WS—BPEL到π—演算整體轉(zhuǎn)換的算法描述。 3．針對(duì)業(yè)務(wù)流程中可能存在的死鎖、活鎖、互模擬問題，本文結(jié)合實(shí)例用π—演算對(duì)業(yè)務(wù)流程性質(zhì)進(jìn)行了分析、推演，并用MWB(Mobility Workbench)進(jìn)行了驗(yàn)證。 4．