0 引言

    人工設計或自動構(gòu)建的系統(tǒng)組合可能存在死鎖,、活鎖等主要問題,，特別是對于復雜信息系統(tǒng),。因此，系統(tǒng)交付前軟件開發(fā)人員必須對信息系統(tǒng)進行嚴格的驗證,，以及時發(fā)現(xiàn)系統(tǒng)組合中存在的問題,。

    目前使用的BPMN(Business Process Model Notation)流程驗證方法主要集中在：(1)BPMN—Petri網(wǎng)映射及驗證；(2)BPMN—Business Process Execution Language(BPEL)映射及驗證,；(3)BPMN—進程代數(shù)映射及驗證等,。

    文獻[1，2]中,，DIJKMAN R M等人提出的方法是將BPMN映射到Petri網(wǎng),。Petri網(wǎng)能揭示系統(tǒng)的許多并發(fā)特性，但是它只有模型而沒有演算^[3],，對于一個復雜的信息系統(tǒng),，若將BPMN模型映射為其對應的Petri網(wǎng)模型也會相對比較復雜，因此,，Petri網(wǎng)對于復雜信息系統(tǒng)的描述有一定的局限性^[4],。文獻[5]展現(xiàn)了BPMN模型如何生成一個BPEL流程，但是采用的是人工方式,，沒有提供一個通用的自動解決方案,。在文獻[6，7]中,，利用業(yè)務流程建模符號(BPMN)建立的業(yè)務流程模型可以直接映射到業(yè)務流程執(zhí)行語言(BPEL4WS),，在業(yè)務流程執(zhí)行引擎中直接運行,但并不是每一個BPMN元素和BPEL元素都可以形成一一對應，所以不可避免地存在映射對應問題,，降低了效率,。還有一些文獻提出了將BPMN映射到進程代數(shù)的方法(如π演算)^[8]，這種方法需要基于MWB（Mobility WorkBench）驗證工具來驗證存在的死鎖,、活鎖和平臺不統(tǒng)一^[9],。

    文中驗證方法直接實現(xiàn)為eclipse的一個插件，可在統(tǒng)一建模平臺上直接處理BPMN模型的輸出,，從BPMN2.0開始直接生成java程序,，有利于系統(tǒng)移植，減少驗證的復雜度,；同時在解決復雜信息系統(tǒng)的信息爆炸方面,，本文實現(xiàn)了優(yōu)化展開算法。

1 研究內(nèi)容

1.1 業(yè)務流程建模

    BPMN2.0體系5種核心元素介紹如下：

    (1)流對象(Connecting Objects)

    活動(Activitics)：企業(yè)所作的工作,活動的類型包括:任務(Task),、進程(Process)和子進程(Sub-Process),。

    事件(Events)：業(yè)務流程的運行過程中發(fā)生的事情。包括啟動事件,、中間事件和結(jié)束事件,。

    網(wǎng)關(guān)(Gateways)：用于控制流程的分支和聚合。使用最多的是互斥網(wǎng)關(guān)和并行網(wǎng)關(guān),。

    (2)連接對象(Connecting Objects)

    順序流(Sequence Flow)：用來表示活動執(zhí)行的順序,。

    關(guān)聯(lián)(Association)：把流對象聯(lián)系起來。關(guān)聯(lián)用于展示活動的輸入和輸出,。

    數(shù)據(jù)關(guān)聯(lián)(Data Association)：用于將數(shù)據(jù)信息與流對象聯(lián)系起來,。

    消息流(Message Flow)：表示兩個實體間消息的傳遞。

    (3)數(shù)據(jù)(Date）

    數(shù)據(jù)對象(Data Objects)：表示活動所需要或產(chǎn)生的數(shù)據(jù),。它們通過關(guān)聯(lián)與活動連接起來,。

    數(shù)據(jù)輸入對象(Data Input Objects)：整個流程中可以被活動讀取的外部數(shù)據(jù)。

    數(shù)據(jù)輸出對象(Data Output Objects)：整個流程的輸出數(shù)據(jù)量,。

    數(shù)據(jù)存儲(Data Store)：整個流程存儲數(shù)據(jù)的地方,，如數(shù)據(jù)庫或文件。

    (4)泳道(Swimlanes)

    池(Pools)：描述流程中的一個參與者,?？煽醋鍪菍⒁幌盗谢顒訁^(qū)別于其他池的一個圖形容器，一般用于B2B建模,。

    道(Lanes)：是池的細分,，代表同一實體的不同部分。

    (5)描述對象(Artifacts)

    組(Group)：用于分析文檔,，不會影響流程,。

    注釋(Annotation)：為了便于理解，提供一些附加性的文本信息,。

1.2 流程到Java代碼的轉(zhuǎn)換

    本文在eclipse平臺集成環(huán)境中設計并驗證BP(Business Process)模型,，eclipse插件的體系結(jié)構(gòu)如圖1所示。

    對于BPMN2.0模型,，使用Xpand引擎給出了Java的形式化語義,，Xpand引擎為每個BPMN2.0模型的元素創(chuàng)建了合適的Java代碼。這個引擎專門用于代碼生成,，它是基于EMF框架和轉(zhuǎn)換模板定義的,。這就意味著能夠從BPMN2.0流程開始直接生成Java程序代碼。為了表示BPMN2.0元素的每個類型（例如開始,、網(wǎng)關(guān),、事件等），介紹了適于支持驗證的每種類型的具體方法,，它們都遵循BPMN2.0的語義,。定義如下方法：

    addPObject（）：一旦Activity被創(chuàng)建就被加到特定的進程中；

    setNext（）：設置它的下一個元素,，定義BP的流向,；

    setMsgToSend（）：用來表示發(fā)送消息的任務,；

    sendMsg（）：是為了指定用setMsgToSend方法定義的Activity發(fā)送一個消息。

2 BPMN流程驗證

2.1 優(yōu)化算法及驗證

    展開算法是一種較好的死鎖檢測的方法,。它是一個偏序規(guī)約的技術(shù),，被廣泛應用到Petri網(wǎng)和進程代數(shù)中，以減少驗證活動中發(fā)生的狀態(tài)爆炸問題,。事實上,，模型的展開算法是無限的，但如果在算法中設置一個特殊的點,，稱之為“結(jié)束前綴”或“截止點”,，一旦構(gòu)造了結(jié)束前綴， 找到識別活鎖狀態(tài)的截止點,，就可以減少對路徑的搜索,，避免狀態(tài)爆炸問題，這樣就實現(xiàn)了展開算法的優(yōu)化,。

2.2 BPMN驗證

2.2.1 活鎖驗證

    對于活鎖的驗證,，利用配置樹找到識別活鎖狀態(tài)的截止點。當且僅當在配置樹的一個祖先節(jié)點的勘探階段已經(jīng)觀察到當前節(jié)點時,，路徑是活鎖,，并標記當前這個點為截止點。截止點的標識可以有效防止復雜信息系統(tǒng)的狀態(tài)爆炸問題,?；铈i的BPMN流程圖如圖2所示。

    圖2 BPMN流程不用轉(zhuǎn)換成狀態(tài)較多的Petri網(wǎng)而生成Main.java,。

    public Main(){

        Process Process_1= new Process("Process_1");

        Activity ExclusiveGateway_1 = new Activity

        (Activity.GATEWAY_EXCLUSIVE); 

        Activity Task_2 = new Activity(Activity.TASK);

        Activity Task_1 = new Activity(Activity.TASK);

        Activity StartEvent_1 = new Activity(Activity.EVENT_START);

        Activity EndEvent_1 = new Activity(Activity.EVENT_END);

        Process_1.addActivity(ExclusiveGateway_1);

        Process_1.addActivity(Task_2);

        Process_1.addActivity(Task_1);

        Process_1.addActivity(StartEvent_1);

        Process_1.addActivity(EndEvent_1);

        ExclusiveGateway_1.setData("EG 1");

        ExclusiveGateway_1.setNext(EndEvent_1);

        ExclusiveGateway_1.setNext(Task_1);

        Task_2.setData("T2");

        Task_2.setNext(ExclusiveGateway_1);

        Task_1.setData("T1");

        Task_1.setNext(Task_2);

        StartEvent_1.setData("S1");

        StartEvent_1.setNext(ExclusiveGateway_1);

            EndEvent_1.setData("E1");

    }

    參照上面的代碼段,，涉及到圖2 Process1中的元素，把Process1中所創(chuàng)建的S1,、EG1,、T1、T2,、E1分別作為不同類型的Activity：START,、GATEWAY_EXCLUSIVE、TASK,、TASK,、END。對每個元素都用setNext方法設置它的下一個元素,；對于發(fā)送消息的任務,，用setMsgToSend方法；發(fā)送消息用sendMsg方法。那么,，對象就添加到程序中了,。圖2示例驗證結(jié)果如圖3所示。

2.2.2 死鎖驗證

    對于死鎖的驗證,，遵循BPMN2.0的終止范式,。在BPMN2.0中，進程執(zhí)行期間,，結(jié)束或終止事件發(fā)生時,，BP才會終止,。從配置中一一刪除結(jié)束事件,，路徑發(fā)生死鎖當且僅當當前配置中有阻塞元素（即任務或事件等待消息并且一個并行網(wǎng)關(guān)等待的輸入流將永遠不會到來），就說明路徑有死鎖發(fā)生,，這種方法也符合展開算法,。死鎖的BPMN流程圖如圖4所示。

    圖4 BPMN流程不用轉(zhuǎn)換成狀態(tài)較多的Petri網(wǎng)而生成Main.java(略),。圖4示例驗證結(jié)果如圖5所示,。

2.3 Petri網(wǎng)驗證BPMN流程

    DIJKMAN R M等人提出的用Petri網(wǎng)驗證BPMN流程是將BPMN模型轉(zhuǎn)換為等價的Petri網(wǎng)模型，BPMN模型在ILOG BPMN Modeler中創(chuàng)建并使用ProM驗證,。

    死鎖,、活鎖定義：Petri網(wǎng)模型的可達圖G=<V：E>是有向圖，頂點集V是Petri 網(wǎng)的狀態(tài)集合{M(P₀,，P₁,，…，P_n)},；

     有向弧E記錄可執(zhí)行變遷及其引起的狀態(tài)遷移,。當遍歷完P(guān)etri網(wǎng)的所有變遷后，庫所能夠到達結(jié)束庫所并且其他的庫所都是空的時,，這個流程是可達的,。當可達樹中，葉子節(jié)點的狀態(tài)標識存在P_i=1但不是結(jié)束庫所的庫所時,，流程存在死鎖,。當可達圖G的任一條路徑L_i=M₀→M₁…M_n(M_i表示庫所變遷后的狀態(tài))表示從初始狀態(tài)到結(jié)束狀態(tài)，那么若任一路徑中存在L_i=M_i→M₁→M₀→M₁…M_j（M_i=M_j）,，則流程存在活鎖^[10],。

2.3.1 Petri網(wǎng)的活鎖驗證

    如圖6所示是圖2的BPMN模型轉(zhuǎn)化為等價的Petri網(wǎng)模型， P₁和t₁是開始庫所和變遷,，P₆和t₆是結(jié)束庫所和變遷,。圖6的Petri網(wǎng)手工模擬分析結(jié)果如圖7所示。

2.3.2 Petri網(wǎng)的死鎖驗證

    如圖8所示是圖4的BPMN模型轉(zhuǎn)化為等價的Petri網(wǎng)模型，用圓圈表示Petri網(wǎng)的庫所,，用長方形表示Petri網(wǎng)的變遷,，P₀和t₀是開始庫所和變遷，P₁₃和t₄是結(jié)束庫所和變遷,。圖8 的Petri網(wǎng)手工模擬分析結(jié)果如圖9所示,。

3 驗證結(jié)果分析

    對比BPMN模型和Petri網(wǎng)模型，如表1,。

    通過以上對兩種驗證死鎖和活鎖方法的比較以及表1,，可得出本文的BPMN直接驗證法優(yōu)點：

    (1)BPMN模型比等價的Petri網(wǎng)模型的圖元總數(shù)少。BPMN模型轉(zhuǎn)換成等價的Petri網(wǎng)模型時,，隨著BPMN模型的復雜度提高,，生成的Petri網(wǎng)模型復雜性也會增加。

    (2)BPMN模型驗證可在統(tǒng)一建模平臺上直接處理BPMN模型輸出,，從BPMN2.0開始直接生成Java程序,，并自動檢驗業(yè)務流程模型中可能存在的死鎖、活鎖,。BPMN模型轉(zhuǎn)換成等價的Petri網(wǎng)模型時,，不可避免地存在映射對應問題，降低了效率,。

    (3)對于一個復雜的信息組合系統(tǒng),，用BPMN模型直接驗證，可采用“截止點”防止狀態(tài)爆炸問題,。但若將BPMN模轉(zhuǎn)換成等價的Petri網(wǎng)模型,，狀態(tài)增多，同時Petri網(wǎng)所引起的狀態(tài)爆炸問題和資源消耗問題很難避免,，對于復雜信息系統(tǒng)的描述有一定的局限性,。

4 結(jié)束語

    本文研究了對BPMN流程的直接驗證方法，并與Petri網(wǎng)驗證作比較,，通過對兩個典型的死鎖,、活鎖例子的整個過程的建模、轉(zhuǎn)換和驗證,，結(jié)果表明對于復雜系統(tǒng),，所提方法可以驗證死鎖、活鎖并有效地避免狀態(tài)爆炸問題和映射問題,，且平臺統(tǒng)一,，可移植性好。今后的工作準備引入π-演算,，在統(tǒng)一平臺上實現(xiàn)π-演算的形式化驗證,。

參考文獻

[1] DIJKMAN R M,，DUMAS M，OUYANG C.Semantics and anaIysis of business proces models in BPMN[J].Information and Software Technology,，2008,，50(12)：1281-1294.

[2] DIJKMAN R M，DUMAS M,，OUYANG C.Formal semantics and anaIysis of BPMN process models using Petri Nets[J].Information and Software Technology,，2008，50(12)：1281-1294.

[3] 錢軍,，馮玉琳．系統(tǒng)動態(tài)行為語義模型及其形式描述[J]．Journal of Computer Research&Development,，1999，36(8)：907-914.

[4] 朱明英.基于BPMN的Web服務組合模型的形式化分析[D].天津：南開大學,，2009.

[5] WHITE S.Using BPMN to model a BPEL process[J].BP Trends,，2005，3(3)：1-18.

[6] 秦天保.從BPMN到可執(zhí)行業(yè)務流程建模[J].計算機應用,，2006(S1)：266-268,，284.

[7] 魏明,，夏永霖,，魏峻.BPMN到BPEL2.0的模型轉(zhuǎn)換方法[J].計算機應用研究，2008(11)：3363-3366.

[8] 云本勝.基于π-演算的信任Web服務組合建模[J].計算機科學,，2012(S3)：240-244.

[9] 李元,，李祥.通信系統(tǒng)演算CCS與自動驗證工具MWB[J].通信技術(shù)，2005(S1)：178-180.

[10] 懷文佳,，劉旭東,，孫海龍，等.一種基于時間Petri網(wǎng)的業(yè)務流程模型驗證方法[C].2010年全國軟件與應用學術(shù)會議(NASAC2010)論文集,，2010：76-81.