基于Petri網的工作流模型合理性驗證

摘要:工作流管理系統具有實時性、同步和異步操作等特點，其建模方法是成功實施工作流管理的關鍵，而工作流模型應該完整地支持工作流定義的概念，正確、高效地反應企業的經營組織過程，為確保工作流的正確運行，必須對工作流模型的合理性進行分析和研究，因此工作流的模型分析和優化成為工作流研究的一個重點[7]。該文從各種研究資料出發，利用工作流模型的合理性定義，給出基于Petri網的工作流模型的驗證步驟和方法。

關鍵詞:工作流;工作流模型;Petri網;模型驗證

中圖分類號:TP311文獻標識碼:A文章編號:1009-3044(2010)11-2603-02

Reasonable Verification of Petri-net Based Workflow Model

WANG Yu1， LI Ceng 2

(1.Anhui Radio and Television University， Hefei 230022， China; 2.Anhui China-Australia Technical and Vocational College， Hefei 230031， China)

Abstract: Workflow management system with real-time， synchronous and asynchronous operation of the characteristics of the successful implementation of their modeling approach is the key to workflow management and workflow model should be complete to support the concept of workflow definition， correct and efficient response to business operations organizational processes， to ensure the correct functioning of the workflow to be the workflow model is reasonable to conduct analysis and research， the workflow modeling and workflow optimization to become a focus of the study. This departure from a variety of research data， using the workflow model’s reasonable definitions given Petri net-based workflow model verification steps and methods.

Key words: workflow;petri-net;model of workflow; model verification

1 工作流模型驗證的意義

應用Petri網的分析技術對工作流模型進行驗證的目的是在過程設計中檢驗工作流的正確性，避免執行時出現異常，過程異常包括死鎖、死任務和活鎖等。工作流建模是開發工作流管理系統的先行任務，所以在工作流投入使用之前就要進行很好的分析驗證。如果一個工作流過程定義模型在其正確性、合理性沒有得到充分驗證時就投入使用，在工作流管理系統運行后再去進行修改，代價將遠遠高于前期的修改。因此在工作流模型實際實施之前，對其進行合理性分析，探索其中可能存在的各種過程異常，可以大大降低工作流運行時停產、檢查和修復的成本，具有重大的意義[1]。

2 工作流網的合理性定義

工作流網的合理性定義是[1，3]:

一個工作流網PN=(P，T，F)建模的過程是合理的，當且僅當滿足下面的三個條件:

1) 對于每一個狀態i可達的狀態M，存在一個實施序列，從狀態M肘通往狀態o，形式化表示為:M(iM)MO;

2) 狀態o是從狀態i可達的唯一最終狀態，且結束時其中至少會有一個標記，形式化表示為:;

3) 在(PN，i)中沒有死活動(不可能執行到的活動)，形式化表示為:?坌t∈T?堝M，Mi'MM'。

其中條件一是規定了從初始庫所總能到達終止庫所;第二個條件規定了當托肯轉移到終止庫所時，其他所有庫所都要是空的，也就意味這整個工作流的結束;第三個條件是規定不能有死活動，即所有的活動都能得到執行。

3 工作流網模型的合理性驗證算法

在研究分析各種文獻的工作流網的合理性驗證理論和方法的基礎上，對原有的算法進行綜合改編，使算法更容易被人所理解，總結出合理性算法的基本思路和驗證步驟[1-2，5]。

算法的基本思路是:根據工作流網模型建立矩陣，用矩陣表示每個活動的前后順序;根據模型表示出每個活動的前后庫所，用來確定托肯轉移時的向量表示規則;從初始庫所出發，根據活動的前后庫所和矩陣判斷后續觸發的活動，并重復此工作，直到沒有活動變遷可以發生;如果終狀態是形如(0，0，…，1)的終止狀態(此時托肯存放在最后一個庫所，其余所有庫所中都沒有托肯存在)，并且所有的活動都觸發過，托肯也經歷了所有的庫所，這時可以說改模型是合理的、正確的，否則模型中就存在錯誤。

在算法中要描述出狀態從(1，0，0，…)到狀態(0，0，…，1)的推算過程，并且要用另一個集合表示所執行的活動，最終檢查是否合理的依據就是a、狀態向量是否變成(0，0，…，1);b、表示活動的集合是否包含所有的活動。算法的具體描述為:

(1) 用矩陣表示各個活動之間的前后順序，方法如下:

(2) 根據矩陣構造各個活動的輸入庫所集合和輸出庫所集合，用·t表示活動t的輸入庫所集合，用t·表示活動t的輸出庫所集合。構造方法是，矩陣t列中所有為1的元素的行號的前驅庫所即t的輸出庫所集合;t行中所有為1的元素的列標的前驅庫所即t的輸入庫所集合;沒有前驅活動的活動的輸入庫所集合為起始庫所i，沒有后續活動的活動的輸出庫所集合為終止庫所o。

(3) 構造初始條件，初始條件有一個向量和一個集合，向量P0=(1，0，0，…)，具體向量的維數是庫所的個數，表示托肯在第一個庫所內;集合T0為空，表示沒有執行任何活動。

(4) 根據活動t的輸入庫所集合·t和輸出庫所集合t·，更改向量P，并把活動t添加到集合T中，并根據矩陣判斷下一個活動。

(5) 反復進行執行步驟(4)，直到沒有活動可以執行且執行一遍所有活動。

4 總結

通過矩陣列舉出活動序列，說明所有的活動都處于起始庫所和終止庫所之間，滿足了合理性條件一;由于在列舉活動序列時，序列中包含了所有活動，說明沒有活動是死活動，滿足了合理性條件三;演算的結果中向量P={0，0，0，0，0，0，0，0，0，1}，證明在工作流結束時，托肯只存在于終止庫所中，其他所有的庫所中均不存在托肯，滿足了合理性條件二。通過以上演算，證明了模型能夠滿足合理性定義中的三個條件，所以可以得出結論，此工作流模型是正確、合理的。[6]

參考文獻:

[1] 郝文，王道平.基于Petri網的工作流建模合理性驗證算法[J].計算機工程與應用，2008，44(13).

[2] van der Aalst W M P.The application of Petri nets to Workflow Management[J].The Journal of Circuits，Systems，and Computers，1998，8(1).

[3] 袁崇義.Petri網原理[M].北京:電子工業出版社，1998.

[4] van der Aalst，W M P.Workflow Management: Models， Methods， and Systems[M].Boston:MIT Press，2002.

[5] 周福明.基于Petri網的工作流建模與正確性分析[J].計算機科學，2005，32(2).

[6] 李嶒.基于Petri網的工作流模型應用研究[D].合肥:安徽大學碩士論文，2008，28-29.

[7] 龐善臣.petri網在工作流系統建模和分析中的應用[J].系統仿真學報，2005(17).