工作流是在计算机辅助下全部或部分自动执行的工作过程。Internet的发展对工作流的发展起了极大的促进作用,使计算机支持的分布式、协同工作的工作流系统在企、事业单位中得到越来越多的应用。在现实世界中设计一个应用工作流是一个复杂而易出错的过程。缺少有效的方法和工具保证工作流的正确性已成为工作流得到进一步广泛应用的一个障碍。 模型检测(Model Checking)是一种采用形式化方法的自动分析和验证技术,相对于传统形式化证明方法,具有快速、准确、全自动、对使用人员数学背景要求不高的特点,目前已在协议验证、分布式系统的设计和验证等方面得到成功的应用,为工作流模型验证提供了新的方法。 本论文研究使用模型检测技术的工作流模型的验证方法。论文首先介绍了工作流相关概念以及模型检测技术的理论和方法,其中对模型检测工具Spin及其输入语言作了较详细的阐述。然后对工作流模型及其UML建模方法进行研究,提出基于UML的以模型检测为目的的工作流模型建模方法,并定义了模型的形式化描述:定义了工作流的形式化模型到Spin/Promela模型的转化规则,使用Spin对工作流模型的结构、语义正确性进行分析和验证。在前面工作的基础上设计了一个基于UML的工作流模型的自动分析和验证的工具,实现由工作流UML模型到Spin/Promela模型的自动转化,使不熟悉模型检测技术的工作者也能使用该方法对工作流进行验证。