工作流是近年来计算机集成制造领域发展最为迅速的技术之一。目前已有多种产品应用于实际中,例如Metero、WIDE等。但由于大多数产品在产品建模过程中缺乏正确性验证或仅进行局部的语法检验,造成工作流模型存在死锁、活锁等缺陷,这直接引发了工作流动态执行过程中的诸多问题,如任务不能完成、超期完成等。因而,在工作流过程定义阶段验证模型的正确性就显得尤为重要。而且在工作流执行前及时发现定义过程中存在的错误可大大降低改正错误的成本。由于工作流模型验证的重要性和必要性,本文基于UML状态图分别建立单个工作流的控制结构、时序约束和数据流模型,并应用形式化方法验证模型正确性。除此之外,还进行了并发工作流的建模与验证。使用UML状态图建立工作流模型,对工作流的控制结构进行验证,包括完全性和语义相关性质两方面。把验证UML状态图的完全性转化为验证全局可达迁移图的完全性,给出了验证控制结构完全性和语义相关性质的算法。在验证工作流时序约束一致性方面,在UML状态图中加入了时间事件,给出了将扩展后的UML状态图转化为时间自动机的规则,用时间计算树逻辑定义了两个任务间的最大、最小时间间隔(上、下界约束)和工作流的最终期限约束,并给出了这三类约束分别在创建阶段、实例化阶段和运行阶段的一致性定义,通过Alur的算法对时序约束一致性进行验证。验证数据流正确性的过程中,在UML状态图中加入了数据流对象,定义了UML状态图的数据流语义,根据该语义给出了从UML状态图到全局状态可达图的转化算法,提出了验证数据流正确性的算法。除了对单个工作流进行建模和验证之外,本文还做了并发工作流方面的建模和验证工作。对UML状态图进行了扩展,描述了从扩展的UML状态图到Büchi自动机的转化过程,并通过Büchi自动机的积建立并发模型,给出了判定在并发模型中是否存在并发冲突的定理,最后给出了验证并发工作流正确性的算法。