军事供应链是由地方经营实体经由军队后勤单位、最终到部队终端用户的一个供应链条。加强军事供应链的管理，是提升军队后勤保障和作战能力的重要方面。在军事供应链运转过程中(尤其是战时)不能发生中断或失效，否则将会导致作战保障任务执行失败，造成严重的后果。为了保证军事供应链持续稳健地运行，其关键任务的正常运行是非常重要的内容。军事供应链关键任务是指军事供应链保障系统中的这样一类任务，在系统运行过程中不能发生中断或失效，否则将对整体作战保障产生重大影响，造成严重后果，其基本特征之一就是在有限执行时间内，在保证所有最重要任务完成的前提下，尽可能多地完成其他关键任务，最大限度地确保整个体系的正常运行。军事供应链体系中有很多关键任务，比如某军港岸基食品保障流程中的领导审批、配备食品、食品运输等任务。根据任务不同的重要程度可将系统中的关键任务分为若干等级，即第一关键任务、第二关键任务等。其中，第一关键任务是为保证系统正常运行必须执行的最重要任务，且系统中至少有一个第一关键任务。之所以需要对关键任务进行等级划分，是因为军事供应链体系存在时间紧迫、保障需求量突增的紧急情况。面对这样一种情况，军事供应链体系对工作流运行的时间约束提出了更严格的要求。 本文主要针对以下两个方面的要求进行研究：一方面，要求整个工作流是在一定时间约束下进行的，并且在截止时间之前确保军事供应链体系的第一关键任务准确完成；另一方面，要求每一个关键任务都要满足自身的时间约束。面对不同等级的关键任务，需对军事供应链体系的工作流进行合理的建模与验证。工作流建模是对军事供应链体系的一种抽象表达，也是其理论研究和实际应用的基础。在军事供应链体系遭受破坏时如何保证现有关键任务持续、及时地完成是当今军事供应链体系工作流需要研究的重要问题。因此，为了确保军事供应链体系持续可靠地运行，对工作流进行建模和验证是两个必不可少的环节。本文采用理论与实践相结合的方法进行研究，基于军事供应链发展的现状与需求，结合工作流的技术与方法，进行相关建模与验证。 二、军事供应链工作流建模与验证的研究现状 从业务流程的角度来看，军事供应链本质上属于工作流。因此，关于军事供应链的建模与验证实际上就是工作流的建模与验证。工作流技术起源于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]。
