0 引言

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

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

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

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

1 研究內容

1.1 業務流程建模

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

    (1)流對象(Connecting Objects)

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

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

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

    (2)連接對象(Connecting Objects)

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

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

    數據關聯(Data Association)：用于將數據信息與流對象聯系起來。

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

    (3)數據(Date）

    數據對象(Data Objects)：表示活動所需要或產生的數據。它們通過關聯與活動連接起來。

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

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

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

    (4)泳道(Swimlanes)

    池(Pools)：描述流程中的一個參與者。可看做是將一系列活動區別于其他池的一個圖形容器，一般用于B2B建模。

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

    (5)描述對象(Artifacts)

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

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

1.2 流程到Java代碼的轉換

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

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

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

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

    setMsgToSend（）：用來表示發送消息的任務；

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

2 BPMN流程驗證

2.1 優化算法及驗證

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

2.2 BPMN驗證

2.2.1 活鎖驗證

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

    圖2 BPMN流程不用轉換成狀態較多的Petri網而生成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中所創建的S1、EG1、T1、T2、E1分別作為不同類型的Activity：START、GATEWAY_EXCLUSIVE、TASK、TASK、END。對每個元素都用setNext方法設置它的下一個元素；對于發送消息的任務，用setMsgToSend方法；發送消息用sendMsg方法。那么，對象就添加到程序中了。圖2示例驗證結果如圖3所示。

2.2.2 死鎖驗證

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

    圖4 BPMN流程不用轉換成狀態較多的Petri網而生成Main.java(略)。圖4示例驗證結果如圖5所示。

2.3 Petri網驗證BPMN流程

    DIJKMAN R M等人提出的用Petri網驗證BPMN流程是將BPMN模型轉換為等價的Petri網模型，BPMN模型在ILOG BPMN Modeler中創建并使用ProM驗證。

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

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

2.3.1 Petri網的活鎖驗證

    如圖6所示是圖2的BPMN模型轉化為等價的Petri網模型， P₁和t₁是開始庫所和變遷，P₆和t₆是結束庫所和變遷。圖6的Petri網手工模擬分析結果如圖7所示。

2.3.2 Petri網的死鎖驗證

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

3 驗證結果分析

    對比BPMN模型和Petri網模型，如表1。

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

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

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

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

4 結束語

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

參考文獻

[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] 錢軍，馮玉琳．系統動態行為語義模型及其形式描述[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到可執行業務流程建模[J].計算機應用，2006(S1)：266-268，284.

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

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

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

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