工作流是一种反应业务流程的计算机化的模型,它是为了在计算机环境支持下实现企业经营过程重组(Business Process Reengineering-BPR)和经营过程自动化(Business Process Automation-BPA)而建立的可由工作流管理系统执行的业务模型。随着计算机技术的发展,对工作流技术的研究应用口益受到学术界与企业界的重视。定义和模拟真实世界中的工作流是一个非常复杂且容易出错的过程,需要一种便于推理验证的方法来进行工作流建模。因此,在设计工作流系统时,通常需要建立一个形式化的工作流模型并通过对形式化模型的模拟和分析来对工作流系统进行验证和优化。尽管目前各经营机构和研究人员已经提出了不少建模方法来描述工作流系统的业务过程,但是对于工作流的模拟执行技术方面仍然需要更加深入的研究。CCS (Calculus of Communicating System)作为进程代数的代表,具有严格的语法和语义规则,因而能够在其基础上对系统的特性进行严格的推理和验证。同时,它的LTS(Labeled Transition Systems)语义描述了CCS模型的状态演化过程,因此可以构造一个等价的自动机模型来描述形式化模型的运行轨迹,对系统进行语义检查。本文的研究以CCS作为理论基础,建立了一个基于CCS的形式化的工作流模型,这个形式化模型能够支持大规模的、复杂的分布式系统中多个组件之间并发协同地工作。根据CCS的LTS语义构造出了与形式化模型语义等价的执行模型,这个执行模型能够对工作流系统语义方面的一些特性进行分析和检查。具体来说,本文的工作包括如下几个方面：(1)建立了一个基于CCS的形式化工作流模型。通过对工作流系统和CCS模型进行分析和比较,能够将工作流系统中的元素与CCS模型中的元素对应起来。工作流中的原子活动对应于CCS中的原子进程,工作流系统中的任务、子工作流和工作流本身对应于复合进程。这样建立起来的形式化工作流模型继承了CCS模型的基本语法和语义。系统中不同的操作者所执行的业务流程、不同厂商生产的工作流产品或组件都可以看作是工作流系统中的子工作流,而CCS所具有的交叠语义能够很好地描述这些子工作流之间的交互。(2)介绍了构造执行模型的方法。这个执行模型描述了形式化模型的执行过程,它实际上是一个有穷自动机。在构造过程中,从初始状态出发,通过追踪复合活动表达式的变化,计算出形式化模型在每个状态下的潜在迁移事件集合,并获得原状态、迁移事件、目的状态之间的映射关系,最终得到形式化模型的运行轨迹,构造出描述形式化模型执行过程的自动机模型。(3)对执行模型的语义正确性进行证明。这部分内容就是证明执行模型与形式化模型是语义等价的。执行模型是通过追踪形式化模型对应的复合表达式在状态迁移过程中的变化而得到的,因此两个模型的语义等价问题可以转化为证明执行模型描述的每一次状态变化都对应于复合表达式的一次变化,复合表达式的每一次变化也对应于执行模型描述的一次状态变化。这样最终就能够证明执行模型是语义正确的。(4)通过一个简单的实例来具体说明应该怎样对工作流系统进行形式化建模,怎样构造形式化工作流模型的执行模型并输出状态图,以及怎样根据执行模型来分析工作流系统的一些特性。根据这个实例可以看出,通过这个执行模型能够检查系统在语义方面的一些特性,如系统行为与预期行为的一致性、系统行为的有效性、安全性等。(5)对本研究工作的总结和展望。事实上,由于π-演算模型是从CCS模型演化发展而来的,本文的研究工作也适用于π-演算模型。