本篇论文的研究是在863计划——“高可信软件生产工具及集成环境”中的子课题5“面向流程管理的软件生产线”的支持下进行的。主要研究方向为工作流过程模型及其能力分析以及正确性验证。虽然工作流管理联盟WFMC为工作流系统提出了一系列参考规范,但实际上并未真正成为各工作流产品所遵守的市场标准,因此目前存在着种类众多的工作流模型和过程定义语言。本文所针对的则为西北大学软件工程研究所提出的信牌驱动工作流模型。自Aalst等人提出了工作流模式的概念后,被普遍用于工作流模型和过程类语言表达能力和适用性的分析与评估。本文首先详细分析了43种过程控制模式在信牌驱动模型中被支持的情况,一方面对原有的信牌驱动模型对业务需求的表达能力给予了肯定,另一方面也发现了其中还存在的一些问题：(1)由于缺乏特定的模型元素因此对一些重要的模式不具备表达能力；(2)对模式的支持程度不高,主要体现在不能完全满足模式的使用约束(如执行期间的安全性)。因此本文将针对原有信牌驱动模型的静态结构及动态执行规则进行必要的修改和扩充,旨在进一步提高模型的表达能力及对过程控制模式的支持程度。文中对信牌驱动模型的静态结构做了形式化定义与研究,主要的成果包括归纳了模型中的五类基本控制结构：顺序结构、split-join结构、split结构、join结构和循环结构及每一种结构的识别算法,另外在五类基本结构的基础上深入研究了结构间的关系和形成原因。在对模型的静态结构的研究上还涉及到一些关键的定义和算法,如主路径及循环路径的定义与查找、聚焦点及聚合点的定义与识别、非循环转移及循环转移的定义与识别、入结构转移及出结构转移的定义与识别等。本文同样以形式化方式定义和研究了模型的执行规则,具体讨论了同步区和非同步区中活动的发生权和发生结果,同时还对过程执行中的多流现象进行了初步研究,主要包括多流形成的原因、出现的位置和多流结构的特点等。在对信牌驱动模型的研究中对转移在3个视角下的分化发挥了关键作用,其中包括基于路径的分化(非循环转移／循环转移)、基于结构的分化(入结构转移／出结构转移)与基于执行规则的分化(一般转移/goback转移),基于转移上的3种分化才得以精确定义模型的静态结构和进一步澄清模型的动态执行规则。本文正是在对模型的形式化研究的基础上,对原有信牌驱动模型进行了适度的改进与扩展,提出了“安全的信牌驱动模型”,主要特点包括：1)对原有信牌驱动模型保持向上兼容；2)对元模型层进行了相应的扩充：增加了SAFE-BLOCKED类型的一致性声明；增加了结构化部分合并、取消部分合并及触发器活动类型；扩充了信牌箱活动的属性,如容量、状态、资源锁属性；扩充了转移的属性,如权值属性和类型属性；这些在元模型层上的改进与扩充进一步提高了模型的表达能力,同时为提高模型在执行上的安全性也提供了基础。3)基于模型静态结构的研究结果,在模型层上解决了模式区域的识别问题；4)基于模型静态结构和动态执行规则的研究结果,定义了安全结构及安全结构的判定规则,并提出了安全执行策略,即从模型结构和执行规则两方面着手,进一步提高了模型的安全性和可靠性。经比较安全的信牌驱动模型比原有的信牌驱动模型在表达能力及对模式的支持程度上都有很大程度的提高。最后,本文还针对安全的信牌驱动模型的验证与仿真做了相关研究和工具实现。实现了在元模型层上的基本语法检查以及在模型层上基于安全结构理论对过程结构进行验证,另外还提出了基于“以路径覆盖为准则的事件生成算法”的仿真策略对过程执行进行分析,以最大程度的发现过程中的各种缺陷,及时修正并优化。目前过程验证与仿真工具的1.0版本已经获得了软件著作权。