0 引言

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

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

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

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

1 研究?jī)?nèi)容

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

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

    (1)流對(duì)象(Connecting Objects)

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

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

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

    (2)連接對(duì)象(Connecting Objects)

    順序流(Sequence Flow)：用來(lái)表示活動(dòng)執(zhí)行的順序。

    關(guān)聯(lián)(Association)：把流對(duì)象聯(lián)系起來(lái)。關(guān)聯(lián)用于展示活動(dòng)的輸入和輸出。

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

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

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

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

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

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

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

    (4)泳道(Swimlanes)

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

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

    (5)描述對(duì)象(Artifacts)

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

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

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

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

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

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

    setNext（）：設(shè)置它的下一個(gè)元素，定義BP的流向；

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

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

2 BPMN流程驗(yàn)證

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

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

2.2 BPMN驗(yàn)證

2.2.1 活鎖驗(yàn)證

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

2.2.2 死鎖驗(yàn)證

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

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

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

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

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

     有向弧E記錄可執(zhí)行變遷及其引起的狀態(tài)遷移。當(dāng)遍歷完P(guān)etri網(wǎng)的所有變遷后，庫(kù)所能夠到達(dá)結(jié)束庫(kù)所并且其他的庫(kù)所都是空的時(shí)，這個(gè)流程是可達(dá)的。當(dāng)可達(dá)樹中，葉子節(jié)點(diǎn)的狀態(tài)標(biāo)識(shí)存在P_i=1但不是結(jié)束庫(kù)所的庫(kù)所時(shí)，流程存在死鎖。當(dāng)可達(dá)圖G的任一條路徑L_i=M₀→M₁…M_n(M_i表示庫(kù)所變遷后的狀態(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)的活鎖驗(yàn)證

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

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

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

3 驗(yàn)證結(jié)果分析

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

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

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

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

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

4 結(jié)束語(yǔ)

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

參考文獻(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)動(dòng)態(tài)行為語(yǔ)義模型及其形式描述[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].計(jì)算機(jī)應(yīng)用，2006(S1)：266-268，284.

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

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

[9] 李元，李祥.通信系統(tǒng)演算CCS與自動(dòng)驗(yàn)證工具M(jìn)WB[J].通信技術(shù)，2005(S1)：178-180.

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