随着软件在信息社会中发挥日益重要的作用,软件的正确性、可靠性、安全性等可信性质越来越多的受到关注。如何在软件的开发和运行过程中保证软件具有高可信性质,这成为软件理论和技术越来越重要的研究方向。国家高技术研究发展计划(863计划)——“高可信软件生产工具及集成环境”中的子课题5“面向流程管理的软件生产线”的一个研究重点即为过程建模、能力分析以及正确性验证。本文的研究重点即为工作流模型的验证。工作流管理系统中的一个关键问题是如何建立一个合理、全面、使用方便和能进行形式化验证的工作流过程模型。为了很好的解决工作流过程建模的问题,本文提出了基于Petri网的扩展信牌驱动工作流模型。该模型具有表达能力强、图形化、使用方便,有严格的形式化语义等特点。工作流管理系统中的另一个重要组成部分是工作流模型验证,目的是在工作流过程实施之前探测其中可能存在的各种错误,从而降低工作过程运行时的停产、检查和修复的成本。本文提出了一种基于Petri网仿真的模型验证方法。该方法弥补了一般基于Petri网模型验证方法的不足,不仅能够验证模型的控制信息,而且可以验证模型的数据信息和资源信息,既可以验证模型的静态结构,又可以验证模型的动态属性。最后,开发出工作流模型验证工具。该工具具有良好的体系结构和友好的人机界面,能够对模型的各种性质进行验证,为模型的优化提供可靠依据。