为了在图论和集合论理论指导下确定方便、实用的工作流模型，论文介绍了基于活动网络的建模技术，给出了活动网络的有向图定义。这种有向图定义可以进一步扩展模型语义，增强模型表达能力。论文讨论了Petri网和扩展Petri网的基本概念、结构特点、活性、静态特性和动态特性的图形表示及示例，研究并实现了从基于活动网络的有向图到扩展Petri网，再从“与分、与汇、或分、或汇”的角度到工作流网的转化算法，给出了工作流建模中四种基本路由的映射规则和实例验证。论文针对扩展Petri网的正确性验证定理。利用自由选择网的一些研究成果，对符合自由选择结构的过程模型，实现了符合自由选择网结构的合理性验证算法。针对通用、直观的工作流网结构的特点，在验证自由选择网正确性的同时，提出了应用Petri网的另一子类来规范、验证工作流网的正确性，从两方面保证了工作流网结构的合理性及正确性同步。最后通过实例讨论了基于Petri网的工作流模型正确性验证算法的实现过程。论文最后总结了课题的研究成果，结合作者的研究方向，提出了进一步的研究目标和展望。