0 引言

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

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

1 研究內(nèi)容

1.1 業(yè)務(wù)流程建模

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

    (1)流對象(Connecting Objects)

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

    事件(Events)：業(yè)務(wù)流程的運行過程中發(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)境中設(shè)計并驗證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（）：設(shè)置它的下一個元素，定義BP的流向；

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

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

2 BPMN流程驗證

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

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

2.2 BPMN驗證

2.2.1 活鎖驗證

    對于活鎖的驗證，利用配置樹找到識別活鎖狀態(tài)的截止點。當且僅當在配置樹的一個祖先節(jié)點的勘探階段已經(jīng)觀察到當前節(jié)點時，路徑是活鎖，并標記當前這個點為截止點。截止點的標識可以有效防止復(fù)雜信息系統(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方法設(shè)置它的下一個元素；對于發(fā)送消息的任務(wù)，用setMsgToSend方法；發(fā)送消息用sendMsg方法。那么，對象就添加到程序中了。圖2示例驗證結(jié)果如圖3所示。

2.2.2 死鎖驗證

    對于死鎖的驗證，遵循BPMN2.0的終止范式。在BPMN2.0中，進程執(zhí)行期間，結(jié)束或終止事件發(fā)生時，BP才會終止。從配置中一一刪除結(jié)束事件，路徑發(fā)生死鎖當且僅當當前配置中有阻塞元素（即任務(wù)或事件等待消息并且一個并行網(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模型的復(fù)雜度提高，生成的Petri網(wǎng)模型復(fù)雜性也會增加。

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

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

4 結(jié)束語

    本文研究了對BPMN流程的直接驗證方法，并與Petri網(wǎng)驗證作比較，通過對兩個典型的死鎖、活鎖例子的整個過程的建模、轉(zhuǎn)換和驗證，結(jié)果表明對于復(fù)雜系統(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服務(wù)組合模型的形式化分析[D].天津：南開大學(xué)，2009.

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

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

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

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

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

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