工作流技术已经成为实现业务流程自动化和重组所必须的技术。工作流建模工具是工作流管理系统的起点,而工作流模型是工作流建模工具设计与实现的基础,工作流模型的正确性验证又是工作流模型能有效描述业务流程的前提和保证。因此,工作流模型及其验证方法的研究对工作流技术的发展有着重要意义。首先,为了提高工作流模型对业务流程的描述能力,对现有的工作流模型进行了分析和比较,对原有的有向图工作流模型进行扩展,引入新的建模元素,提出了基于扩展条件有向图的工作流模型。给出了扩展条件有向图工作流模型的形式化定义和图形符号描述,并通过一个研究实例详细说明了使用扩展条件有向图工作流模型进行建模的过程。其次,为了验证工作流模型结构的正确性,将Pi-Calculus引入到模型验证的过程中,给出了如何使用Pi-Calculus描述所建立的工作流模型。在使用Pi-Calculus准确描述模型的基础上,提出了基于Pi-Calculus的工作流模型归约规则,给出了基于Pi-Calculus归约规则的工作流模型验证算法和验证方法,给出了验证算法的时间复杂度分析和验证方法的正确性分析。最后,以扩展条件有向图工作流模型和基于Pi-Calulus归约规则的工作流验证方法为基础,设计并开发了一个工作流建模工具(YsuSoftWF),并给出了工作流建模工具的功能需求和YsuSoftWF设计的系统框架,给出了如何使用YsuSoftWF进行可视化建模及相关属性的设置,并且给出了YsuSoftWF工具在电子政务领域的具体应用,展示了如何将YsuSoftWF应用到实际项目的开发与实现的过程中,体现了YsuSoftWF在具体项目中的应用价值,同时证实了扩展条件有向图工作流模型和基于Pi-Calulus归约规则的工作流模型验证方法是可以满足实际需求的。