论文部分内容阅读
基于BPEL的工作流技术,在企业流程的管理上应用越来越广泛。为基于BPEL的工作流模型的模拟和分析提出一个框架,并给出检查用BPEL实现的工作流程正确性的方法。讨论问题主要三个:(1)如何使一个用BPEL语言实现的工作流模型可以转化为数据流网络模型;(2)如何能潜在地把不正确执行路径纳入;(3)如何用SPIN能将工作流的性能形式化地验证出来。为了实现从工作流到分析模型转变的步骤.使用了图形转变,实现分两个步骤实施工作流程-PROMELA转型,使每一个较小的一步都在抽象的水平。此验证方法方便于模型设计,而且