基于關(guān)鍵任務(wù)的軍事供應(yīng)鏈工作流建模與驗(yàn)證方法研究

王洪達(dá) 蔣麗華 楊曼

摘 要：為保證軍事供應(yīng)鏈能夠持續(xù)穩(wěn)健地運(yùn)行，其關(guān)鍵任務(wù)的正常運(yùn)行是非常重要的內(nèi)容。軍事供應(yīng)鏈關(guān)鍵任務(wù)是指軍事供應(yīng)鏈保障系統(tǒng)中的這樣一類任務(wù)，在系統(tǒng)運(yùn)行過(guò)程中不能發(fā)生中斷或失效，否則將對(duì)整體作戰(zhàn)保障產(chǎn)生重大影響，造成嚴(yán)重后果。其基本特征之一就是在有限執(zhí)行時(shí)間內(nèi)，在保證所有最重要任務(wù)完成的前提下，盡可能多地完成其他關(guān)鍵任務(wù)，最大限度地確保整個(gè)系統(tǒng)的正常運(yùn)行。因此，需要對(duì)軍事供應(yīng)鏈中的工作流（任務(wù)流）進(jìn)行有效的建模和驗(yàn)證。然而，目前的建模與驗(yàn)證方法大多只解決了確定性的工作流建模與驗(yàn)證，忽略了不確定因素（供應(yīng)商的不穩(wěn)定、緊急任務(wù)執(zhí)行的突發(fā)性等）對(duì)軍事供應(yīng)鏈的影響。因此，文章針對(duì)軍事供應(yīng)鏈關(guān)鍵任務(wù)的工作流建模與驗(yàn)證問(wèn)題展開(kāi)研究，以期提高軍事供應(yīng)鏈業(yè)務(wù)流程的可信性和可靠性，實(shí)現(xiàn)在任務(wù)執(zhí)行周期內(nèi)提供持續(xù)可用的功能服務(wù)以及軍事供應(yīng)鏈的管理與優(yōu)化調(diào)度。

關(guān) 鍵 詞：軍事供應(yīng)鏈;關(guān)鍵任務(wù);工作流;建模;驗(yàn)證

一、 引言

軍事供應(yīng)鏈?zhǔn)怯傻胤浇?jīng)營(yíng)實(shí)體經(jīng)由軍隊(duì)后勤單位、最終到部隊(duì)終端用戶的一個(gè)供應(yīng)鏈條。加強(qiáng)軍事供應(yīng)鏈的管理，是提升軍隊(duì)后勤保障和作戰(zhàn)能力的重要方面。在軍事供應(yīng)鏈運(yùn)轉(zhuǎn)過(guò)程中（尤其是戰(zhàn)時(shí)）不能發(fā)生中斷或失效，否則將會(huì)導(dǎo)致作戰(zhàn)保障任務(wù)執(zhí)行失敗，造成嚴(yán)重的后果。為了保證軍事供應(yīng)鏈持續(xù)穩(wěn)健地運(yùn)行，其關(guān)鍵任務(wù)的正常運(yùn)行是非常重要的內(nèi)容。軍事供應(yīng)鏈關(guān)鍵任務(wù)是指軍事供應(yīng)鏈保障系統(tǒng)中的這樣一類任務(wù)，在系統(tǒng)運(yùn)行過(guò)程中不能發(fā)生中斷或失效，否則將對(duì)整體作戰(zhàn)保障產(chǎn)生重大影響，造成嚴(yán)重后果，其基本特征之一就是在有限執(zhí)行時(shí)間內(nèi)，在保證所有最重要任務(wù)完成的前提下，盡可能多地完成其他關(guān)鍵任務(wù)，最大限度地確保整個(gè)體系的正常運(yùn)行。軍事供應(yīng)鏈體系中有很多關(guān)鍵任務(wù)，比如某軍港岸基食品保障流程中的領(lǐng)導(dǎo)審批、配備食品、食品運(yùn)輸?shù)热蝿?wù)。根據(jù)任務(wù)不同的重要程度可將系統(tǒng)中的關(guān)鍵任務(wù)分為若干等級(jí)，即第一關(guān)鍵任務(wù)、第二關(guān)鍵任務(wù)等。其中，第一關(guān)鍵任務(wù)是為保證系統(tǒng)正常運(yùn)行必須執(zhí)行的最重要任務(wù)，且系統(tǒng)中至少有一個(gè)第一關(guān)鍵任務(wù)。之所以需要對(duì)關(guān)鍵任務(wù)進(jìn)行等級(jí)劃分，是因?yàn)檐娛鹿?yīng)鏈體系存在時(shí)間緊迫、保障需求量突增的緊急情況。面對(duì)這樣一種情況，軍事供應(yīng)鏈體系對(duì)工作流運(yùn)行的時(shí)間約束提出了更嚴(yán)格的要求。

本文主要針對(duì)以下兩個(gè)方面的要求進(jìn)行研究：一方面，要求整個(gè)工作流是在一定時(shí)間約束下進(jìn)行的，并且在截止時(shí)間之前確保軍事供應(yīng)鏈體系的第一關(guān)鍵任務(wù)準(zhǔn)確完成;另一方面，要求每一個(gè)關(guān)鍵任務(wù)都要滿足自身的時(shí)間約束。面對(duì)不同等級(jí)的關(guān)鍵任務(wù)，需對(duì)軍事供應(yīng)鏈體系的工作流進(jìn)行合理的建模與驗(yàn)證。工作流建模是對(duì)軍事供應(yīng)鏈體系的一種抽象表達(dá)，也是其理論研究和實(shí)際應(yīng)用的基礎(chǔ)。在軍事供應(yīng)鏈體系遭受破壞時(shí)如何保證現(xiàn)有關(guān)鍵任務(wù)持續(xù)、及時(shí)地完成是當(dāng)今軍事供應(yīng)鏈體系工作流需要研究的重要問(wèn)題。因此，為了確保軍事供應(yīng)鏈體系持續(xù)可靠地運(yùn)行，對(duì)工作流進(jìn)行建模和驗(yàn)證是兩個(gè)必不可少的環(huán)節(jié)。本文采用理論與實(shí)踐相結(jié)合的方法進(jìn)行研究，基于軍事供應(yīng)鏈發(fā)展的現(xiàn)狀與需求，結(jié)合工作流的技術(shù)與方法，進(jìn)行相關(guān)建模與驗(yàn)證。

二、軍事供應(yīng)鏈工作流建模與驗(yàn)證的研究現(xiàn)狀

從業(yè)務(wù)流程的角度來(lái)看，軍事供應(yīng)鏈本質(zhì)上屬于工作流。因此，關(guān)于軍事供應(yīng)鏈的建模與驗(yàn)證實(shí)際上就是工作流的建模與驗(yàn)證。工作流技術(shù)起源于20世紀(jì)70年代中期辦公和生產(chǎn)組織自動(dòng)化領(lǐng)域的研究。它是根據(jù)固定業(yè)務(wù)流程而提出的。在計(jì)算機(jī)網(wǎng)絡(luò)環(huán)境下，工作流是通過(guò)將任務(wù)細(xì)化分解為更小的子任務(wù)，并根據(jù)所給出的規(guī)則及過(guò)程來(lái)運(yùn)行，同時(shí)也可以對(duì)其任務(wù)的運(yùn)行情況進(jìn)行監(jiān)控[1]。隨著信息化水平的迅速發(fā)展，系統(tǒng)對(duì)其工作流建模技術(shù)的要求也在不斷地提高，自20世紀(jì)末以來(lái)，國(guó)內(nèi)外專家學(xué)者對(duì)于工作流模型方法的研究一直非常關(guān)注。

1998年，Geppert提出了將活動(dòng)實(shí)例和過(guò)程實(shí)例兩個(gè)元素運(yùn)用到工作流中[2]，建立了具有動(dòng)態(tài)性的模型，并對(duì)工作流模型的動(dòng)態(tài)性展開(kāi)了全面的分析和研究。2000年，孫志瑞和史美林[3]試圖運(yùn)用XOR-Split和Choice-Merge等組織結(jié)構(gòu)將工作流程中的每一種可能路徑都描述出來(lái)，并對(duì)其進(jìn)行定義。這一方法的缺點(diǎn)非常明顯，就是會(huì)導(dǎo)致整個(gè)模型變得非常龐大以至于讓人難以理解。除此之外，這一方法的前提是要知道模型中所有不確定因素后才可對(duì)流程進(jìn)行定義，而這一要求是不現(xiàn)實(shí)的。為了避免這一方法的局限性，陳曙等（2009）[4]提出了Black Box、Packet等概念，該方法將模型中無(wú)法確定的因素進(jìn)行封裝，減小了模型的規(guī)模，但新元素（如Packet）的引入也使得工作流模型更加復(fù)雜?；贏alst et al.[5]研究中的不足，Sadiq et al.[6]提出利用ER圖（entity relationship diagram）對(duì)工作流元模型進(jìn)行改進(jìn)，并用形式化語(yǔ)言對(duì)模型進(jìn)行描述和動(dòng)態(tài)分析。近些年，研究人員對(duì)工作流建模方法有了新的見(jiàn)解。從2000年至今，越來(lái)越多的建模元素被應(yīng)用于工作流建模中，如進(jìn)程代數(shù)、Petri網(wǎng)、自動(dòng)機(jī)，這些元素大大增加了工作流的建模效率，加強(qiáng)了系統(tǒng)運(yùn)行的穩(wěn)定性。另外，為了提高工作流建模的可靠性，國(guó)內(nèi)外研究專家不斷地完善建模方法。當(dāng)前，較多有效可靠的工作流建模方法被提出，如簡(jiǎn)海青（2012）[7]對(duì)工作流元模型進(jìn)行深入分析并設(shè)計(jì)了工作流動(dòng)態(tài)修改的步驟。部分文獻(xiàn)提出了一種基于進(jìn)程代數(shù)的工作流建模方法[4，8]。柳楊（2017）、石少玲（2016）和陳莉萍（2016）提出了一種基于自動(dòng)機(jī)的工作流建模方法，并運(yùn)用實(shí)際案例對(duì)所提方法進(jìn)行驗(yàn)證[9-11]。單繼城等[12]提出了基于著色Petri網(wǎng)的混合工作流建模方法，并采用模塊聚合方式給出了混合工作流的層次CPN模型。除此之外，部分文獻(xiàn)分別針對(duì)不同的應(yīng)用場(chǎng)景，提出了基于Petri網(wǎng)的工作流建模方法[13-17]。

面對(duì)不確定環(huán)境下的工作流模型，對(duì)其進(jìn)行可靠性驗(yàn)證是將模型投入現(xiàn)實(shí)運(yùn)營(yíng)之前必不可少的一步。當(dāng)前，對(duì)信息化保障系統(tǒng)工作流模型進(jìn)行驗(yàn)證的研究還比較少，尤其是對(duì)所有可能模型的可靠性驗(yàn)證方法更是不存在。針對(duì)一些包含特殊結(jié)構(gòu)的工作流，2000年Sadiq et al.[18]提出將復(fù)雜龐大的工作流模型先化簡(jiǎn)后驗(yàn)證的方法，該方法利用總結(jié)歸納的五種化簡(jiǎn)規(guī)則對(duì)工作流的死鎖進(jìn)行了驗(yàn)證。在此研究基礎(chǔ)上，他們還提出了一種判定工作流模型結(jié)構(gòu)可靠性的方法。另外，針對(duì)Geppert[2]無(wú)法檢測(cè)出工作流模型中的沖突結(jié)構(gòu)，Lin et al.[19]和宋寶燕等[20]分別提出了一種圖形規(guī)約的過(guò)程模型驗(yàn)證方法并對(duì)模型中的沖突結(jié)構(gòu)進(jìn)行檢測(cè)。除了以上對(duì)圖形化簡(jiǎn)的驗(yàn)證方法外，Aalst 提出運(yùn)用Petri網(wǎng)對(duì)系統(tǒng)工作流進(jìn)行建模并對(duì)模型的可行性進(jìn)行驗(yàn)證。在文獻(xiàn)Verification of Workflow Nets中，他首次提出利用Petri網(wǎng)對(duì)模型進(jìn)行化簡(jiǎn)，然后再對(duì)模型的性質(zhì)進(jìn)行驗(yàn)證，但文中只給出了簡(jiǎn)要步驟，并未能完全解決工作流的驗(yàn)證問(wèn)題[21]。在近些年的研究中，國(guó)內(nèi)外專家學(xué)者對(duì)基于Petri網(wǎng)的工作流建模與驗(yàn)證方法進(jìn)行了深入的研究，比如周建濤等[22]提出用Petri網(wǎng)將工作流的過(guò)程語(yǔ)義進(jìn)行化簡(jiǎn)并驗(yàn)證;劉惠義等[23]將時(shí)間著色Petri網(wǎng)與圖規(guī)約法則相結(jié)合，提出了一種工作流驗(yàn)證方法;Wang et al. and Chang et al.運(yùn)用Petri網(wǎng)對(duì)模型的完整性進(jìn)行了系統(tǒng)的驗(yàn)證等[24-25]。

三、軍事供應(yīng)鏈關(guān)鍵任務(wù)的工作流建模與驗(yàn)證方法研究框架

本文主要對(duì)軍事供應(yīng)鏈體系業(yè)務(wù)保障流程關(guān)鍵任務(wù)的工作流建模與驗(yàn)證方法進(jìn)行研究。建模與驗(yàn)證看似互相獨(dú)立，但實(shí)則兩者相輔相成。建模是驗(yàn)證的基礎(chǔ)，而驗(yàn)證又是建模的保障，因此兩者有著密切的聯(lián)系。軍事供應(yīng)鏈體系的工作流建模是在高可信、高生存以及高可用的環(huán)境下運(yùn)行的，在有限的時(shí)間約束內(nèi)，利用著色Petri網(wǎng)，并將系統(tǒng)中的關(guān)鍵任務(wù)進(jìn)行等級(jí)分類，從而對(duì)軍事供應(yīng)鏈關(guān)鍵任務(wù)的工作流進(jìn)行建模。在建模過(guò)程中為了避免模型有誤而產(chǎn)生巨大損失，需要對(duì)模型的特性進(jìn)行可靠性驗(yàn)證。因此，本文對(duì)工作流模型的狀態(tài)空間、可調(diào)度性和時(shí)間約束的驗(yàn)證方法進(jìn)行了研究。

本文的總體研究思路，如圖1所示。研究背景是在軍事供應(yīng)鏈體系下進(jìn)行的，主要研究?jī)?nèi)容為關(guān)鍵任務(wù)的工作流建模與驗(yàn)證兩個(gè)方面。其中，工作流建模是基于著色Petri網(wǎng)和死路徑消除語(yǔ)義進(jìn)行的。另外，工作流驗(yàn)證是從以下方面進(jìn)行：首先，對(duì)模型的狀態(tài)空間和可調(diào)度性進(jìn)行驗(yàn)證;其次，對(duì)模型進(jìn)行時(shí)間約束驗(yàn)證，并且對(duì)最優(yōu)路徑進(jìn)行了分析;最后，通過(guò)某軍事供應(yīng)鏈體系應(yīng)用案例，驗(yàn)證本文所提出方法的實(shí)用性和可靠性。

（一）軍事供應(yīng)鏈關(guān)鍵任務(wù)工作流建模

工作流技術(shù)應(yīng)用越來(lái)越廣泛，其中，工作流建模是基于著色Petri網(wǎng)和死路徑消除語(yǔ)義進(jìn)行的。軍事供應(yīng)鏈關(guān)鍵任務(wù)的工作流建模技術(shù)也在不斷走向成熟，然而在工作流的建模過(guò)程存在著一些難點(diǎn)。軍事供應(yīng)鏈工作流復(fù)雜多變，如何利用工作流技術(shù)定義任務(wù)關(guān)鍵系統(tǒng)中的關(guān)鍵任務(wù)、如何定義死路徑消除語(yǔ)義對(duì)于建模工作來(lái)講都是挑戰(zhàn)。

結(jié)合以上所提出的問(wèn)題和要求，本文在前期已有工作的基礎(chǔ)上，提出一種死路徑消除語(yǔ)義下的軍事供應(yīng)鏈系統(tǒng)關(guān)鍵任務(wù)的工作流建模方法，運(yùn)用著色Petri網(wǎng)對(duì)所建立的死路徑消除語(yǔ)義轉(zhuǎn)化為普通“if-then-else”的規(guī)則進(jìn)行描述。其中，顏色集代表關(guān)鍵任務(wù)的重要性，并采用CPN-Tools工具將其形式化地展示出來(lái)。

（二）軍事供應(yīng)鏈關(guān)鍵任務(wù)工作流狀態(tài)空間及可調(diào)度性驗(yàn)證方法研究

軍事供應(yīng)鏈系統(tǒng)是一個(gè)具備高可信、高生存以及高可用等特性的系統(tǒng)。在現(xiàn)實(shí)應(yīng)用中，系統(tǒng)的關(guān)鍵任務(wù)執(zhí)行時(shí)間都是有限且準(zhǔn)確的。如何在時(shí)間有限的情況下確保系統(tǒng)中的關(guān)鍵任務(wù)持續(xù)、高效地完成，已成為亟待研究和解決的問(wèn)題。時(shí)間約束下軍事供應(yīng)鏈系統(tǒng)關(guān)鍵任務(wù)的可行性分析，也就是確保有限時(shí)間約束內(nèi)能夠完成任務(wù)的觸發(fā)問(wèn)題。換句話說(shuō)，模型投入運(yùn)行前必須驗(yàn)證所有關(guān)鍵任務(wù)的狀態(tài)空間性質(zhì)和可調(diào)度性。

工作流模型具有可調(diào)度性，是指模型中任意兩個(gè)變遷之間不存在潛在資源的沖突。對(duì)于定義的任意等級(jí)的關(guān)鍵任務(wù)而言，可以通過(guò)修正沖突活動(dòng)的時(shí)間約束以使得該工作流的不可調(diào)度活動(dòng)變成可調(diào)度活動(dòng)，從而使該工作流可調(diào)度性良好。經(jīng)過(guò)調(diào)研分析，本文推薦使用時(shí)間約束Petri網(wǎng)來(lái)進(jìn)行建模。時(shí)間約束Petri網(wǎng)可以定義任意時(shí)間的活動(dòng)，并進(jìn)行可調(diào)度性分析。因此，在框架中擬研究一種基于時(shí)間約束著色Petri網(wǎng)的軍事供應(yīng)鏈關(guān)鍵任務(wù)的工作流可調(diào)度性驗(yàn)證及其修正策略。

（三）軍事供應(yīng)鏈關(guān)鍵任務(wù)工作流時(shí)間約束驗(yàn)證方法研究

隨著軍事供應(yīng)鏈系統(tǒng)關(guān)鍵任務(wù)對(duì)時(shí)間約束要求的不斷提高，時(shí)間約束下系統(tǒng)的建模問(wèn)題也日益成為研究焦點(diǎn)，而系統(tǒng)的建模本質(zhì)上也是一個(gè)工作流過(guò)程的建模。為了使得工作流建模更加簡(jiǎn)潔明了，并解決時(shí)間驗(yàn)證這一問(wèn)題，本文運(yùn)用時(shí)間約束著色Petri網(wǎng)對(duì)軍事供應(yīng)鏈系統(tǒng)關(guān)鍵任務(wù)的工作流進(jìn)行時(shí)間約束下的建模與驗(yàn)證。

目前，工作流所面臨的最重要的挑戰(zhàn)就是工作流的時(shí)間管理問(wèn)題，工作流管理系統(tǒng)（workflow management system，WFMS）針對(duì)這一問(wèn)題并未給出準(zhǔn)確的定義。但在實(shí)際案例應(yīng)用中，尤其是對(duì)運(yùn)行時(shí)間要求極其嚴(yán)格的軍事供應(yīng)鏈系統(tǒng)來(lái)說(shuō)，其工作流的時(shí)間約束驗(yàn)證問(wèn)題顯得尤為重要。當(dāng)前，一些關(guān)于工作流的時(shí)間驗(yàn)證研究都集中在對(duì)于基本工作流的驗(yàn)證，很少考慮任務(wù)關(guān)鍵系統(tǒng)工作流的時(shí)間驗(yàn)證問(wèn)題。雖然有些學(xué)者對(duì)于時(shí)間約束下的工作流過(guò)程進(jìn)行了幾種基本結(jié)構(gòu)下的時(shí)間驗(yàn)證分析，但這些并不能很好運(yùn)用在計(jì)算機(jī)運(yùn)行中。在近些年的研究中，很多學(xué)者將工作流程進(jìn)行建模和時(shí)間驗(yàn)證，但并未將兩者與最優(yōu)路徑的分析相結(jié)合。因此，本文的研究框架的第三點(diǎn)是在已有工作的基礎(chǔ)上利用著色時(shí)間Petri網(wǎng)的建模優(yōu)勢(shì)，將其與任務(wù)關(guān)鍵系統(tǒng)工作流相結(jié)合，運(yùn)用時(shí)間約束著色Petri網(wǎng)建模軍事供應(yīng)鏈任務(wù)關(guān)鍵系統(tǒng)，對(duì)其工作流的基本結(jié)構(gòu)進(jìn)行分析。基于此，建立適合基本結(jié)構(gòu)的時(shí)間驗(yàn)證規(guī)則，并在有限時(shí)間約束條件下研究最優(yōu)時(shí)間的分析策略。

四、 結(jié)論

軍事供應(yīng)鏈系統(tǒng)需要考慮各種不確定因素的影響，以滿足復(fù)雜多變環(huán)境下必須及時(shí)完成任務(wù)的需求。其中，系統(tǒng)中任務(wù)的可調(diào)度性是其運(yùn)行的前提因素。除此之外，軍事供應(yīng)鏈系統(tǒng)也會(huì)對(duì)系統(tǒng)中的任務(wù)進(jìn)行時(shí)間約束，從而提高運(yùn)行效率。因此，在對(duì)任務(wù)關(guān)鍵系統(tǒng)的工作流進(jìn)行建模后，為了保證軍事供應(yīng)鏈系統(tǒng)安全可靠地運(yùn)行，需要對(duì)工作流的基本性質(zhì)進(jìn)行充分的驗(yàn)證。本文系統(tǒng)地分析了現(xiàn)有軍事供應(yīng)鏈關(guān)鍵任務(wù)的研究現(xiàn)狀，并在此基礎(chǔ)上提出了一個(gè)完整的研究框架。

參考文獻(xiàn)：

[1]范玉順.工作流管理技術(shù)基礎(chǔ)實(shí)現(xiàn)企業(yè)業(yè)務(wù)過(guò)程重組、過(guò)程管理與過(guò)程自動(dòng)化的核心技術(shù)[M].北京：清華大學(xué)出版社，2001.

[2]GEPPERT A，TOMBROS D，DITTRICH K R.Defining the semantics of reactive components in event-driven workflow execution with event histories[J].Information systems，1998，23（3-4）：235-252.

[3]孫志瑞，史美林.一個(gè)支持動(dòng)態(tài)變化的工作流元模型[J].電子學(xué)報(bào)，2002，30 （12A）：2052-2056.

[4]陳曙，毋國(guó)慶，肖晶.一種進(jìn)程代數(shù)風(fēng)格的基于時(shí)序邏輯的工作流建模方法[C]// 2009國(guó)際信息技與應(yīng)用論壇，2009.

[5]AALST W M P V D，BARROS A P，HOFSTEDE A H M T，et al.Advanced workflow patterns[C]// International Conference on Cooperative Information Systems.Springer-Verlag，2000：18-29.

[6]SADIQ S，SADIQ W，ORLOWSKA M.Pockets of flexibility in workflow specification[M]// Conceptual modeling — ER 2001.Berlin：Springer，2001：513-526.

[7]簡(jiǎn)海青.基于Petri網(wǎng)的動(dòng)態(tài)工作流建模方法的研究與實(shí)現(xiàn)[D].廣州：華南理工大學(xué)，2012.

[8]FOSTERH，UCHITEL S，MAGEE J，et al.Model-based verification of web service compositions[C]// IEEE International Conference on Automated Software Engineering，2003.Proceedings.IEEE，2003：152-161.

[9]柳楊.基于時(shí)間自動(dòng)機(jī)的列控中心建模與半實(shí)物仿真[D].北京：北京交通大學(xué)，2017.

[10]石少玲.基于時(shí)間自動(dòng)機(jī)的嵌入式工業(yè)控制系統(tǒng)建模與分析[D].昆明：昆明理工大學(xué)，2016.

[11]陳莉萍.Web服務(wù)組合中事務(wù)驅(qū)動(dòng)的服務(wù)選擇有限自動(dòng)機(jī)[J].渭南師范學(xué)院學(xué)報(bào)，2016，31（12）：41-45.

[12]單繼城，黃光奇，王德鑫，等.基于著色Petri網(wǎng)的混合工作流建模及合理性分析[J].信息工程大學(xué)學(xué)報(bào)，2015，16（2）：218-224.

[13]湯澤宇.基于Petri網(wǎng)的工作流并行算法的研究與實(shí)現(xiàn)[D].南寧：廣西師范學(xué)院，2016.

[14]徐沛東.基于Petri網(wǎng)的建筑市場(chǎng)監(jiān)管工作流設(shè)計(jì)與實(shí)現(xiàn)[D].鄭州：鄭州大學(xué)，2016.

[15]林程華.基于Petri網(wǎng)的工作流技術(shù)在審批流程中的應(yīng)用[J].電腦編程技巧與維護(hù)，2017（3）：22-24.

[16]張丹，佘維.基于Petri網(wǎng)的電力系統(tǒng)監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核方法[J].計(jì)算機(jī)測(cè)量與控制，2016，24（4）：101-104.

[17]HOLLINGSWORTH D.Workflow management coalition：the workflow reference model[Z].Hampshire：The Workflow Management Coalition，1993.

[18]SADIQ W，ORLOWSK A M.Analyzing process models using graph reduction techniques[J].Information systems，2000，25（2）：117-134.

[19]LIN H，ZHAO Z，LI H，et al.A novel graph reduction algorithm to identify structural conflicts[C]// Hawaii International Conference on System Sciences.IEEE，2002：10.

[20]宋寶燕，王菊英，于戈.基于圖形展開(kāi)及圖形歸約的過(guò)程模型驗(yàn)證方法[J].小型微型計(jì)算機(jī)系統(tǒng)，2005，26（6）：1073-1078.

[21]AALST W M P VAN DER.Verification of workflow nets[M]// Application and theory of petri nets 1997.Berlin ：Springer，1997：407-426.

[22]周建濤，史美林，葉新銘.一種基于Petri網(wǎng)化簡(jiǎn)的工作流過(guò)程語(yǔ)義驗(yàn)證方法[J].軟件學(xué)報(bào)，2005，16（7）：1242-1251.

[23]劉惠義，吳繼鋒，曾曉勤.基于圖規(guī)約法的TCPN工作流網(wǎng)模型的驗(yàn)證方法[J].系統(tǒng)仿真學(xué)報(bào)，2006，18（10）：2976-2979.

[24]WANG J，XIA Z，DING Y.A method for soundness verification of workflow model based on petri net[C]// International Conference on Computer Science & Education.IEEE，2009：880-883.

[25]CHANG G，YANG H，RONGM O.A new method for business process verification based on petri-net[J].Journal of Sichuan University，2016（6）.