基于关键任务的军事供应链工作流建模与验证方法研究

王洪达 蒋丽华 杨曼

摘 要：为保证军事供应链能够持续稳健地运行，其关键任务的正常运行是非常重要的内容。军事供应链关键任务是指军事供应链保障系统中的这样一类任务，在系统运行过程中不能发生中断或失效，否则将对整体作战保障产生重大影响，造成严重后果。其基本特征之一就是在有限执行时间内，在保证所有最重要任务完成的前提下，尽可能多地完成其他关键任务，最大限度地确保整个系统的正常运行。因此，需要对军事供应链中的工作流（任务流）进行有效的建模和验证。然而，目前的建模与验证方法大多只解决了确定性的工作流建模与验证，忽略了不确定因素（供应商的不稳定、紧急任务执行的突发性等）对军事供应链的影响。因此，文章针对军事供应链关键任务的工作流建模与验证问题展开研究，以期提高军事供应链业务流程的可信性和可靠性，实现在任务执行周期内提供持续可用的功能服务以及军事供应链的管理与优化调度。

关 键 词：军事供应链;关键任务;工作流;建模;验证

一、 引言

军事供应链是由地方经营实体经由军队后勤单位、最终到部队终端用户的一个供应链条。加强军事供应链的管理，是提升军队后勤保障和作战能力的重要方面。在军事供应链运转过程中（尤其是战时）不能发生中断或失效，否则将会导致作战保障任务执行失败，造成严重的后果。为了保证军事供应链持续稳健地运行，其关键任务的正常运行是非常重要的内容。军事供应链关键任务是指军事供应链保障系统中的这样一类任务，在系统运行过程中不能发生中断或失效，否则将对整体作战保障产生重大影响，造成严重后果，其基本特征之一就是在有限执行时间内，在保证所有最重要任务完成的前提下，尽可能多地完成其他关键任务，最大限度地确保整个体系的正常运行。军事供应链体系中有很多关键任务，比如某军港岸基食品保障流程中的领导审批、配备食品、食品运输等任务。根据任务不同的重要程度可将系统中的关键任务分为若干等级，即第一关键任务、第二关键任务等。其中，第一关键任务是为保证系统正常运行必须执行的最重要任务，且系统中至少有一个第一关键任务。之所以需要对关键任务进行等级划分，是因为军事供应链体系存在时间紧迫、保障需求量突增的紧急情况。面对这样一种情况，军事供应链体系对工作流运行的时间约束提出了更严格的要求。

本文主要针对以下两个方面的要求进行研究：一方面，要求整个工作流是在一定时间约束下进行的，并且在截止时间之前确保军事供应链体系的第一关键任务准确完成;另一方面，要求每一个关键任务都要满足自身的时间约束。面对不同等级的关键任务，需对军事供应链体系的工作流进行合理的建模与验证。工作流建模是对军事供应链体系的一种抽象表达，也是其理论研究和实际应用的基础。在军事供应链体系遭受破坏时如何保证现有关键任务持续、及时地完成是当今军事供应链体系工作流需要研究的重要问题。因此，为了确保军事供应链体系持续可靠地运行，对工作流进行建模和验证是两个必不可少的环节。本文采用理论与实践相结合的方法进行研究，基于军事供应链发展的现状与需求，结合工作流的技术与方法，进行相关建模与验证。

二、军事供应链工作流建模与验证的研究现状

从业务流程的角度来看，军事供应链本质上属于工作流。因此，关于军事供应链的建模与验证实际上就是工作流的建模与验证。工作流技术起源于20世纪70年代中期办公和生产组织自动化领域的研究。它是根据固定业务流程而提出的。在计算机网络环境下，工作流是通过将任务细化分解为更小的子任务，并根据所给出的规则及过程来运行，同时也可以对其任务的运行情况进行监控[1]。随着信息化水平的迅速发展，系统对其工作流建模技术的要求也在不断地提高，自20世纪末以来，国内外专家学者对于工作流模型方法的研究一直非常关注。

1998年，Geppert提出了将活动实例和过程实例两个元素运用到工作流中[2]，建立了具有动态性的模型，并对工作流模型的动态性展开了全面的分析和研究。2000年，孙志瑞和史美林[3]试图运用XOR-Split和Choice-Merge等组织结构将工作流程中的每一种可能路径都描述出来，并对其进行定义。这一方法的缺点非常明显，就是会导致整个模型变得非常庞大以至于让人难以理解。除此之外，这一方法的前提是要知道模型中所有不确定因素后才可对流程进行定义，而这一要求是不现实的。为了避免这一方法的局限性，陈曙等（2009）[4]提出了Black Box、Packet等概念，该方法将模型中无法确定的因素进行封装，减小了模型的规模，但新元素（如Packet）的引入也使得工作流模型更加复杂。基于Aalst et al.[5]研究中的不足，Sadiq et al.[6]提出利用ER图（entity relationship diagram）对工作流元模型进行改进，并用形式化语言对模型进行描述和动态分析。近些年，研究人员对工作流建模方法有了新的见解。从2000年至今，越来越多的建模元素被应用于工作流建模中，如进程代数、Petri网、自动机，这些元素大大增加了工作流的建模效率，加强了系统运行的稳定性。另外，为了提高工作流建模的可靠性，国内外研究专家不断地完善建模方法。当前，较多有效可靠的工作流建模方法被提出，如简海青（2012）[7]对工作流元模型进行深入分析并设计了工作流动态修改的步骤。部分文献提出了一种基于进程代数的工作流建模方法[4，8]。柳杨（2017）、石少玲（2016）和陈莉萍（2016）提出了一种基于自动机的工作流建模方法，并运用实际案例对所提方法进行验证[9-11]。单继城等[12]提出了基于着色Petri网的混合工作流建模方法，并采用模块聚合方式给出了混合工作流的层次CPN模型。除此之外，部分文献分别针对不同的应用场景，提出了基于Petri网的工作流建模方法[13-17]。

面对不确定环境下的工作流模型，对其进行可靠性验证是将模型投入现实运营之前必不可少的一步。当前，对信息化保障系统工作流模型进行验证的研究还比较少，尤其是对所有可能模型的可靠性验证方法更是不存在。针对一些包含特殊结构的工作流，2000年Sadiq et al.[18]提出将复杂庞大的工作流模型先化简后验证的方法，该方法利用总结归纳的五种化简规则对工作流的死锁进行了验证。在此研究基础上，他们还提出了一种判定工作流模型结构可靠性的方法。另外，针对Geppert[2]无法检测出工作流模型中的冲突结构，Lin et al.[19]和宋宝燕等[20]分别提出了一种图形规约的过程模型验证方法并对模型中的冲突结构进行检测。除了以上对图形化简的验证方法外，Aalst 提出运用Petri网对系统工作流进行建模并对模型的可行性进行验证。在文献Verification of Workflow Nets中，他首次提出利用Petri网对模型进行化简，然后再对模型的性质进行验证，但文中只给出了简要步骤，并未能完全解决工作流的验证问题[21]。在近些年的研究中，國内外专家学者对基于Petri网的工作流建模与验证方法进行了深入的研究，比如周建涛等[22]提出用Petri网将工作流的过程语义进行化简并验证;刘惠义等[23]将时间着色Petri网与图规约法则相结合，提出了一种工作流验证方法;Wang et al. and Chang et al.运用Petri网对模型的完整性进行了系统的验证等[24-25]。

三、军事供应链关键任务的工作流建模与验证方法研究框架

本文主要对军事供应链体系业务保障流程关键任务的工作流建模与验证方法进行研究。建模与验证看似互相独立，但实则两者相辅相成。建模是验证的基础，而验证又是建模的保障，因此两者有着密切的联系。军事供应链体系的工作流建模是在高可信、高生存以及高可用的环境下运行的，在有限的时间约束内，利用着色Petri网，并将系统中的关键任务进行等级分类，从而对军事供应链关键任务的工作流进行建模。在建模过程中为了避免模型有误而产生巨大损失，需要对模型的特性进行可靠性验证。因此，本文对工作流模型的状态空间、可调度性和时间约束的验证方法进行了研究。

本文的总体研究思路，如图1所示。研究背景是在军事供应链体系下进行的，主要研究内容为关键任务的工作流建模与验证两个方面。其中，工作流建模是基于着色Petri网和死路径消除语义进行的。另外，工作流验证是从以下方面进行：首先，对模型的状态空间和可调度性进行验证;其次，对模型进行时间约束验证，并且对最优路径进行了分析;最后，通过某军事供应链体系应用案例，验证本文所提出方法的实用性和可靠性。

（一）军事供应链关键任务工作流建模

工作流技术应用越来越广泛，其中，工作流建模是基于着色Petri网和死路径消除语义进行的。军事供应链关键任务的工作流建模技术也在不断走向成熟，然而在工作流的建模过程存在着一些难点。军事供应链工作流复杂多变，如何利用工作流技术定义任务关键系统中的关键任务、如何定义死路径消除语义对于建模工作来讲都是挑战。

结合以上所提出的问题和要求，本文在前期已有工作的基础上，提出一种死路径消除语义下的军事供应链系统关键任务的工作流建模方法，运用着色Petri网对所建立的死路径消除语义转化为普通“if-then-else”的规则进行描述。其中，颜色集代表关键任务的重要性，并采用CPN-Tools工具将其形式化地展示出来。

（二）军事供应链关键任务工作流状态空间及可调度性验证方法研究

军事供应链系统是一个具备高可信、高生存以及高可用等特性的系统。在现实应用中，系统的关键任务执行时间都是有限且准确的。如何在时间有限的情况下确保系统中的关键任务持续、高效地完成，已成为亟待研究和解决的问题。时间约束下军事供应链系统关键任务的可行性分析，也就是确保有限时间约束内能够完成任务的触发问题。换句话说，模型投入运行前必须验证所有关键任务的状态空间性质和可调度性。

工作流模型具有可调度性，是指模型中任意两个变迁之间不存在潜在资源的冲突。对于定义的任意等级的关键任务而言，可以通过修正冲突活动的时间约束以使得该工作流的不可调度活动变成可调度活动，从而使该工作流可调度性良好。经过调研分析，本文推荐使用时间约束Petri网来进行建模。时间约束Petri网可以定义任意时间的活动，并进行可调度性分析。因此，在框架中拟研究一种基于时间约束着色Petri网的军事供应链关键任务的工作流可调度性验证及其修正策略。

（三）军事供应链关键任务工作流时间约束验证方法研究

随着军事供应链系统关键任务对时间约束要求的不断提高，时间约束下系统的建模问题也日益成为研究焦点，而系统的建模本质上也是一个工作流过程的建模。为了使得工作流建模更加简洁明了，并解决时间验证这一问题，本文运用时间约束着色Petri网对军事供应链系统关键任务的工作流进行时间约束下的建模与验证。

目前，工作流所面临的最重要的挑战就是工作流的时间管理问题，工作流管理系统（workflow management system，WFMS）针对这一问题并未给出准确的定义。但在实际案例应用中，尤其是对运行时间要求极其严格的军事供应链系统来说，其工作流的时间约束验证问题显得尤为重要。当前，一些关于工作流的时间验证研究都集中在对于基本工作流的验证，很少考虑任务关键系统工作流的时间验证问题。虽然有些学者对于时间约束下的工作流过程进行了几种基本结构下的时间验证分析，但这些并不能很好运用在计算机运行中。在近些年的研究中，很多学者将工作流程进行建模和时间验证，但并未将两者与最优路径的分析相结合。因此，本文的研究框架的第三点是在已有工作的基础上利用着色时间Petri网的建模优势，将其与任务关键系统工作流相结合，运用时间约束着色Petri网建模军事供应链任务关键系统，对其工作流的基本结构进行分析。基于此，建立适合基本结构的时间验证规则，并在有限时间约束条件下研究最优时间的分析策略。

四、 结论

軍事供应链系统需要考虑各种不确定因素的影响，以满足复杂多变环境下必须及时完成任务的需求。其中，系统中任务的可调度性是其运行的前提因素。除此之外，军事供应链系统也会对系统中的任务进行时间约束，从而提高运行效率。因此，在对任务关键系统的工作流进行建模后，为了保证军事供应链系统安全可靠地运行，需要对工作流的基本性质进行充分的验证。本文系统地分析了现有军事供应链关键任务的研究现状，并在此基础上提出了一个完整的研究框架。

参考文献：

[1]范玉顺.工作流管理技术基础实现企业业务过程重组、过程管理与过程自动化的核心技术[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]孙志瑞，史美林.一个支持动态变化的工作流元模型[J].电子学报，2002，30 （12A）：2052-2056.

[4]陈曙，毋国庆，肖晶.一种进程代数风格的基于时序逻辑的工作流建模方法[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网的动态工作流建模方法的研究与实现[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]石少玲.基于时间自动机的嵌入式工业控制系统建模与分析[D].昆明：昆明理工大学，2016.

[11]陈莉萍.Web服务组合中事务驱动的服务选择有限自动机[J].渭南师范学院学报，2016，31（12）：41-45.

[12]单继城，黄光奇，王德鑫，等.基于着色Petri网的混合工作流建模及合理性分析[J].信息工程大学学报，2015，16（2）：218-224.

[13]汤泽宇.基于Petri网的工作流并行算法的研究与实现[D].南宁：广西师范学院，2016.

[14]徐沛东.基于Petri网的建筑市场监管工作流设计与实现[D].郑州：郑州大学，2016.

[15]林程华.基于Petri网的工作流技术在审批流程中的应用[J].电脑编程技巧与维护，2017（3）：22-24.

[16]张丹，佘维.基于Petri网的电力系统监控数据多点校核方法[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].小型微型计算机系统，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]刘惠义，吴继锋，曾晓勤.基于图规约法的TCPN工作流网模型的验证方法[J].系统仿真学报，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）.