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

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

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

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

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