基于可替換性Petri網(wǎng)工作流模型合理性驗(yàn)證

時(shí)慧晶，李 雄

（昆明船舶設(shè)備研究試驗(yàn)中心，昆明650051）

基于可替換性Petri網(wǎng)工作流模型合理性驗(yàn)證

時(shí)慧晶，李 雄

（昆明船舶設(shè)備研究試驗(yàn)中心，昆明650051）

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

工作流模型；結(jié)構(gòu)合理性；工作流網(wǎng)；可替換性

1 引 言

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

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

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

3 基于WF-net可替換性的合理性驗(yàn)證法

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

WF-net的可替換特性，為驗(yàn)證復(fù)雜工作流模型的結(jié)構(gòu)合理性提供了新思路：針對待驗(yàn)證的WF-net PN，首先構(gòu)造一組規(guī)模較小、結(jié)構(gòu)簡單的基本W(wǎng)F-net，并運(yùn)用可達(dá)樹分析方法對其進(jìn)行合理性分析，確保它們是合理并且安全的，稱為“構(gòu)造塊”。基于這組構(gòu)造塊，以待驗(yàn)證的WF-net PN為目標(biāo)，進(jìn)行一定次序的替換構(gòu)造，如果可以得到與PN結(jié)構(gòu)相同的WF-net，則證明PN是合理并且安全的。

4 公文發(fā)文工作流模型合理性分析

通過對昆明船舶設(shè)備研究試驗(yàn)中心的公文發(fā)文過程進(jìn)行分析，利用著色時(shí)間Petri網(wǎng)建立其工作流模型，如圖1所示。

圖1 基于著色時(shí)間Petri網(wǎng)的公文發(fā)文工作流模型

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

圖2 經(jīng)過等效變換后的公文發(fā)文工作流

4.1 基本構(gòu)造塊及其合理性驗(yàn)證模型

為了使用基于可替換性的模型合理性驗(yàn)證法進(jìn)行WF-net合理性驗(yàn)證，針對公文發(fā)文工作流模型，首先構(gòu)造如圖3所示的一組結(jié)構(gòu)簡單、規(guī)模較小的基本W(wǎng)F-net。

由于上述這組WF-net結(jié)構(gòu)簡單，可以運(yùn)用可達(dá)樹分析法進(jìn)行合理性分析。圖4是利用可達(dá)樹構(gòu)造算法得到對應(yīng)的可達(dá)樹。

通過分析上圖各可達(dá)樹，可以得出：

（1）在各可達(dá)樹的葉節(jié)點(diǎn)中，除了結(jié)束庫所外，其余所有庫所中標(biāo)記數(shù)均為0，因此四種基本W(wǎng)F-net能夠正常終止；

（2）各可達(dá)樹中不存在標(biāo)記數(shù)始終為0的庫所，所以四種基本W(wǎng)F-net中沒有死鎖，均具有活性；

（3）對于各可達(dá)樹的每個(gè)節(jié)點(diǎn)，庫所中標(biāo)記的最大數(shù)目不超過1，所以四種基本W(wǎng)F-net是有界并且安全的。

上述三點(diǎn)證明了這組WF-net是合理并且安全的，因此可以稱它們?yōu)闃?gòu)造塊。當(dāng)然，可能還有其它符合要求的構(gòu)造塊，但是對于公文發(fā)文工作流模型來說，這組構(gòu)造塊的功能已經(jīng)足夠強(qiáng)大。

4.2 公文發(fā)文工作流模型的構(gòu)造步驟

為了驗(yàn)證公文發(fā)文工作流模型的合理性，通過上述四種構(gòu)造塊，按照一定的次序試圖去分步構(gòu)造公文發(fā)文工作流模型。

圖3 一組結(jié)構(gòu)簡單的基本W(wǎng)F-net

圖4 基本W(wǎng)F-net對應(yīng)的可達(dá)樹

第一步，開始構(gòu)造，應(yīng)用圖5所示的基本結(jié)構(gòu)構(gòu)造塊，其中x＝t1。

圖5 開始構(gòu)造：應(yīng)用一個(gè)基本結(jié)構(gòu)構(gòu)造塊

第二步，連續(xù)應(yīng)用兩個(gè)圖6所示的順序結(jié)構(gòu)，在變遷t1后增加變遷t2和t4。

圖6 連續(xù)應(yīng)用兩個(gè)順序結(jié)構(gòu)

第三步，對t2應(yīng)用圖3中的循環(huán)結(jié)構(gòu)，其中x＝t2，y＝t3。得到如7圖所示W(wǎng)F-net。

圖7 對t2應(yīng)用一個(gè)循環(huán)結(jié)構(gòu)

第四步，對變遷t4應(yīng)用一個(gè)圖3中的選擇結(jié)構(gòu)，增加變遷t6，其中x＝t4，y＝t6，如圖8所示。

第五步，再對t4應(yīng)用一個(gè)循環(huán)結(jié)構(gòu)，增加變遷t5。其中x＝t4，y＝t5，得到如下的WF-net，如圖9所示。

圖8 對t4應(yīng)用一個(gè)選擇結(jié)構(gòu)

圖9 對t4應(yīng)用一個(gè)循環(huán)結(jié)構(gòu)

第六步，采用順序結(jié)構(gòu)，在變遷 t6后增加變遷t7。

5 結(jié)束語

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

圖10 對t6應(yīng)用循環(huán)結(jié)構(gòu)

［1］高茜.活的單支Petri網(wǎng)的可達(dá)性判定方法及改進(jìn)的可覆蓋性樹的構(gòu)造算法［D］.濟(jì)南：山東大學(xué)，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］劉婷，林闖，劉衛(wèi)東.基于時(shí)間Petri網(wǎng)的工作流系統(tǒng)模型的線性推理［J］.電子學(xué)報(bào)，2002，30（2）：153-156.

［4］郎艷麗，劉婷，林闖.人事檔案管理系統(tǒng)及其時(shí)間Petri網(wǎng)工作流模型［J］.計(jì)算機(jī)工程與應(yīng)用，2001，37（18）：153-156.

［5］曾艷林.基于Petri網(wǎng)的工作流過程建模的研究［D］.大連：大連海事大學(xué)，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

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

2013-11-11