復(fù)雜信息系統(tǒng)流程驗(yàn)證及統(tǒng)一建模平臺實(shí)現(xiàn)研究.pdf

1、復(fù)雜信息系統(tǒng)的流程復(fù)雜，并發(fā)性強(qiáng)，分支結(jié)點(diǎn)多，系統(tǒng)完成后發(fā)現(xiàn)系統(tǒng)存在問題，更改系統(tǒng)代價(jià)會很大，所以應(yīng)對系統(tǒng)進(jìn)行建模，檢查系統(tǒng)流程中存在的死鎖和活鎖。業(yè)務(wù)流程管理倡議組織(BPMI，The Business Process Management Initiative)開發(fā)了一套標(biāo)準(zhǔn)的業(yè)務(wù)流程建模符號(BPMN-Business Process Model and Notation)，它是一套圖形化和用戶友好型業(yè)務(wù)流程符號。但是，由于BPM

2、N是半形式化型語言，自身無法進(jìn)行推導(dǎo)演算來查找模型中存在的問題，所以，需要提出方法對BPMN模型進(jìn)行驗(yàn)證。而模型檢測是對狀態(tài)空間的窮舉搜索，對于并發(fā)性強(qiáng)的復(fù)雜信息系統(tǒng)來說，狀態(tài)爆炸是不可避免的，所以，應(yīng)該找出減小狀態(tài)爆炸幾率的方法。
　　為了解決業(yè)務(wù)流程設(shè)計(jì)、形式化分析、驗(yàn)證的平臺不統(tǒng)一，可移植性差等問題，提出了一種在統(tǒng)一建模平臺上處理BPMN模型輸出的業(yè)務(wù)流程形式化驗(yàn)證方案。首先構(gòu)建基于Java語言的形式化建模平臺，將BPMN模

3、型輸出作為該平臺的輸入，隨后輸出基于BPMN2.0業(yè)務(wù)流程形式化驗(yàn)證的Java程序代碼；該代碼可在本文構(gòu)建的建模平臺實(shí)現(xiàn)自動檢驗(yàn)業(yè)務(wù)流程模型中可能存在的死鎖、活鎖，并通過設(shè)置“截止點(diǎn)”來解決由活鎖引起的狀態(tài)爆炸問題。文中最后給出了復(fù)雜信息系統(tǒng)的相應(yīng)的實(shí)例，驗(yàn)證了方案的有效性。下面是本文主要研究的幾個方面，包括：
　　1.分析了Petri網(wǎng)和π-演算的業(yè)務(wù)流程驗(yàn)證方法，總結(jié)出BPMN模型的核心元素到Petri網(wǎng)的映射以及BPMN模型

4、核心元素到π-演算的映射，得出這兩種驗(yàn)證方法存在平臺不統(tǒng)一問題，并提出在統(tǒng)一Eclipse平臺上建模BPMN業(yè)務(wù)流程并完成驗(yàn)證工作的方法。
　　2.根據(jù)各種驗(yàn)證算法的映射思想將BPMN模型的核心元素封裝成java類后，建模的BPMN模型可先轉(zhuǎn)換成java代碼，然后對**.java文件進(jìn)行死鎖和活鎖的驗(yàn)證。
　　3.在展開算法中加入“截止點(diǎn)”的標(biāo)識，當(dāng)流程識別到“截止點(diǎn)”時(shí)終止對流程中相同路徑的遍歷，從而減小狀態(tài)爆炸的幾率。<