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

1、復(fù)雜信息系統(tǒng)的流程復(fù)雜，并發(fā)性強，分支結(jié)點多，系統(tǒng)完成后發(fā)現(xiàn)系統(tǒng)存在問題，更改系統(tǒng)代價會很大，所以應(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)行驗證。而模型檢測是對狀態(tài)空間的窮舉搜索，對于并發(fā)性強的復(fù)雜信息系統(tǒng)來說，狀態(tài)爆炸是不可避免的，所以，應(yīng)該找出減小狀態(tài)爆炸幾率的方法。
　　為了解決業(yè)務(wù)流程設(shè)計、形式化分析、驗證的平臺不統(tǒng)一，可移植性差等問題，提出了一種在統(tǒng)一建模平臺上處理BPMN模型輸出的業(yè)務(wù)流程形式化驗證方案。首先構(gòu)建基于Java語言的形式化建模平臺，將BPMN模

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

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