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

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

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

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