王洪達 蔣麗華 楊曼

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

關 鍵 詞：軍事供應鏈;關鍵任務;工作流;建模;驗證

一、 引言

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

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

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

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

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

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

三、軍事供應鏈關鍵任務的工作流建模與驗證方法研究框架

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

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

（一）軍事供應鏈關鍵任務工作流建模

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

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

（二）軍事供應鏈關鍵任務工作流狀態(tài)空間及可調度性驗證方法研究

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

工作流模型具有可調度性，是指模型中任意兩個變遷之間不存在潛在資源的沖突。對于定義的任意等級的關鍵任務而言，可以通過修正沖突活動的時間約束以使得該工作流的不可調度活動變成可調度活動，從而使該工作流可調度性良好。經過調研分析，本文推薦使用時間約束Petri網來進行建模。時間約束Petri網可以定義任意時間的活動，并進行可調度性分析。因此，在框架中擬研究一種基于時間約束著色Petri網的軍事供應鏈關鍵任務的工作流可調度性驗證及其修正策略。

（三）軍事供應鏈關鍵任務工作流時間約束驗證方法研究

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

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

四、 結論

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

參考文獻：

[1]范玉順.工作流管理技術基礎實現(xiàn)企業(yè)業(yè)務過程重組、過程管理與過程自動化的核心技術[M].北京：清華大學出版社，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]孫志瑞，史美林.一個支持動態(tài)變化的工作流元模型[J].電子學報，2002，30 （12A）：2052-2056.

[4]陳曙，毋國慶，肖晶.一種進程代數(shù)風格的基于時序邏輯的工作流建模方法[C]// 2009國際信息技與應用論壇，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]簡海青.基于Petri網的動態(tài)工作流建模方法的研究與實現(xiàn)[D].廣州：華南理工大學，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]柳楊.基于時間自動機的列控中心建模與半實物仿真[D].北京：北京交通大學，2017.

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

[11]陳莉萍.Web服務組合中事務驅動的服務選擇有限自動機[J].渭南師范學院學報，2016，31（12）：41-45.

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

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

[14]徐沛東.基于Petri網的建筑市場監(jiān)管工作流設計與實現(xiàn)[D].鄭州：鄭州大學，2016.

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

[16]張丹，佘維.基于Petri網的電力系統(tǒng)監(jiān)控數(shù)據多點校核方法[J].計算機測量與控制，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]宋寶燕，王菊英，于戈.基于圖形展開及圖形歸約的過程模型驗證方法[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網化簡的工作流過程語義驗證方法[J].軟件學報，2005，16（7）：1242-1251.

[23]劉惠義，吳繼鋒，曾曉勤.基于圖規(guī)約法的TCPN工作流網模型的驗證方法[J].系統(tǒng)仿真學報，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）.