基于可替換性Petri網工作流模型合理性驗證

時慧晶，李 雄

（昆明船舶設備研究試驗中心，昆明650051）

基于可替換性Petri網工作流模型合理性驗證

時慧晶，李 雄

（昆明船舶設備研究試驗中心，昆明650051）

所謂工作流是一類能夠完全或者部分自動執行的業務過程，它根據一系列過程規則、文檔、信息或任務能夠在不同的執行者之間傳遞、執行，模型結構的合理性對于工作流來說是至關重要的。提出一種基于WF-net可替換性模型結構合理性驗證方法，通過合理且安全的構造塊分步構造模型，最終完成對模型的合理性驗證。通過對昆明船舶設備研究試驗中心的公文發文過程進行分析，利用著色時間Petri網建立工作流模型無需冗雜的計算，此方法適合于復雜工作流模型的合理性驗證。

工作流模型；結構合理性；工作流網；可替換性

1 引 言

所謂工作流是一類能夠完全或者部分自動執行的業務過程，它根據一系列過程規則、文檔、信息或任務能夠在不同的執行者之間傳遞、執行。本文提出一種基于WF-net可替換性的模型結構合理性驗證方法，該方法通過合理且安全的構造塊，分步構造模型，最終完成對模型的合理性驗證。此方法無需冗雜的計算，整個過程直觀易懂，適合于復雜工作流模型的合理性驗證。

2 工作流模型的合理性定義

對工作流的控制流維度進行建模的Petri網被稱做工作流網（WF-net），即利用Petri網對工作流過程進行定義得到的網。對于一個復雜的WF-net來說，僅憑定義判定其合理性顯然不容易。合理性對應于活性和有界性［1］。為了將合理性和活性、有界性聯系起來，我們定義一個擴展WF-net：給定WF-net PN＝（P，T，F），增加一個額外的變遷t′，使t′連接結束庫所o和起始庫所i，其中o是t′的輸入庫所、i是t′的輸出庫所，這樣得到的網稱為擴展WF-net。在擴展WF-net的基礎上，在Petri網判定為活的且是有界的定理中［2］，對WF-net的合理性驗證就被轉換成對Petri網相關屬性分析，可運用Petri網豐富的分析手段去驗證WF-net的合理性。

3 基于WF-net可替換性的合理性驗證法

工作流的層次特性可以被用來判定一個WF-net的結構合理性：有兩個合理的而且安全的WF-net PN1和PN2，PN1里面的任務t′恰好只有一個輸入和一個輸出，然后用PN2替換PN1里面的任務t′，此時t′不再是一個簡單的任務而是對一個子過程的引用，這樣得到的WF-net PN3也是合理并且安全的［3］。可以理解為一個合理的WF-net，其行為類似于一個變遷：從輸入庫所取得一個標記，經過一段時間后生成一個標記放入其輸出庫所中。

WF-net的可替換特性，為驗證復雜工作流模型的結構合理性提供了新思路：針對待驗證的WF-net PN，首先構造一組規模較小、結構簡單的基本WF-net，并運用可達樹分析方法對其進行合理性分析，確保它們是合理并且安全的，稱為“構造塊”。基于這組構造塊，以待驗證的WF-net PN為目標，進行一定次序的替換構造，如果可以得到與PN結構相同的WF-net，則證明PN是合理并且安全的。

4 公文發文工作流模型合理性分析

通過對昆明船舶設備研究試驗中心的公文發文過程進行分析，利用著色時間Petri網建立其工作流模型，如圖1所示。

圖1 基于著色時間Petri網的公文發文工作流模型

由于在分析模型結構合理性時，只關注標記在WF-net中的流動，不涉及到顏色集和變遷時延［4］，因此在正式進行合理性驗證之前，忽略公文發文處理工作流模型中的顏色集和各個變遷的時延，并對其做出如圖2所示的等效變換，使模型的結構更加清晰直觀。

圖2 經過等效變換后的公文發文工作流

4.1 基本構造塊及其合理性驗證模型

為了使用基于可替換性的模型合理性驗證法進行WF-net合理性驗證，針對公文發文工作流模型，首先構造如圖3所示的一組結構簡單、規模較小的基本WF-net。

由于上述這組WF-net結構簡單，可以運用可達樹分析法進行合理性分析。圖4是利用可達樹構造算法得到對應的可達樹。

通過分析上圖各可達樹，可以得出：

（1）在各可達樹的葉節點中，除了結束庫所外，其余所有庫所中標記數均為0，因此四種基本WF-net能夠正常終止；

（2）各可達樹中不存在標記數始終為0的庫所，所以四種基本WF-net中沒有死鎖，均具有活性；

（3）對于各可達樹的每個節點，庫所中標記的最大數目不超過1，所以四種基本WF-net是有界并且安全的。

上述三點證明了這組WF-net是合理并且安全的，因此可以稱它們為構造塊。當然，可能還有其它符合要求的構造塊，但是對于公文發文工作流模型來說，這組構造塊的功能已經足夠強大。

4.2 公文發文工作流模型的構造步驟

為了驗證公文發文工作流模型的合理性，通過上述四種構造塊，按照一定的次序試圖去分步構造公文發文工作流模型。

圖3 一組結構簡單的基本WF-net

圖4 基本WF-net對應的可達樹

第一步，開始構造，應用圖5所示的基本結構構造塊，其中x＝t1。

圖5 開始構造：應用一個基本結構構造塊

第二步，連續應用兩個圖6所示的順序結構，在變遷t1后增加變遷t2和t4。

圖6 連續應用兩個順序結構

第三步，對t2應用圖3中的循環結構，其中x＝t2，y＝t3。得到如7圖所示WF-net。

圖7 對t2應用一個循環結構

第四步，對變遷t4應用一個圖3中的選擇結構，增加變遷t6，其中x＝t4，y＝t6，如圖8所示。

第五步，再對t4應用一個循環結構，增加變遷t5。其中x＝t4，y＝t5，得到如下的WF-net，如圖9所示。

圖8 對t4應用一個選擇結構

圖9 對t4應用一個循環結構

第六步，采用順序結構，在變遷 t6后增加變遷t7。

5 結束語

通過六步構造最終得到如圖10所示的WF-net。得到的WF-net與公文發文工作流模型完全一致。根據定理［5］可以判定公文發文工作流模型是合理且安全的。

圖10 對t6應用循環結構

［1］高茜.活的單支Petri網的可達性判定方法及改進的可覆蓋性樹的構造算法［D］.濟南：山東大學，2008：12-14.

［2］Xiao Jun，Deng Haihong，Gao Yunfeng，Zhou Chungui，Liu Lei.Workflow modeling and time performance analysis based on Petri net［J］.Journal of Jilin University，2009，27（1）：104-120.

［3］劉婷，林闖，劉衛東.基于時間Petri網的工作流系統模型的線性推理［J］.電子學報，2002，30（2）：153-156.

［4］郎艷麗，劉婷，林闖.人事檔案管理系統及其時間Petri網工作流模型［J］.計算機工程與應用，2001，37（18）：153-156.

［5］曾艷林.基于Petri網的工作流過程建模的研究［D］.大連：大連海事大學，2007：45-47.

Rationality Validation Based on Exchangeable Petri NetWork File Model

SHIHui-jing，LIXiong
（Kunming Ship-borne Equipment Research and Test Center，Kunming 650051，China）

The work file，as a kind of operation process，which can be executed automatically or selfautomatically，is impressed and implemented among different operators according to a series of rules，files，information or assignment.The rationality ofmodel structure plays an important role to work file.The rationality validation method based on exchangeableWF-netmodel is proposed in this paper.The structuremodel is established steeply by reasonable and safe structure block.At last，the final rationality validation is accomplished for the model.Through analyzing the document dispatch process of Kunming ship-borne Equipment Research and Test Center，the chromatic time Petrinet is used to setup work file modelwithoutmiscellaneous computing，which fits for the validation of complicated WF-netmodel.

Work filemode；Structure rationality；WF-net exchangeability

10.3969／j.issn.1002-2279.2014.03.006

TP301.2

：A

：1002-2279（2014）03-0018-03

時慧晶（1986-），女，山東德州人，工學碩士，助理工程師，主研方向：從事保障設備及發控技術方向的研究。

2013-11-11