工作流过程建模中的形式化验证技术

开篇：润墨网以专业的文秘视角，为您筛选了一篇工作流过程建模中的形式化验证技术范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！

【摘要】本文阐述了工作流概念，工作流验证方法的研究现状，随后，进行了工作流模型的验证分析，最后，针对工作流过程建模中的形式化验证技术提出了进一步的研究方向。

【关键词】工作流过程；建模；形式化验证；技术

中图分类号： TU198 文献标识码： A 文章编号：

一、前言

工作流过程建模中的形式化验证对于我们更好的使用工作流有重要的意义，对于工作流过程建模中的形式化验证，我们需要使用科学、合理的验证方式来展开对工作流工程建模中的形式化验证。

二、工作流概述

工作流（ Foundare WorkFlow）就是工作流程的计算模型，即将工作流程中的工作如何前后组织在一起的逻辑和规则在计算机中以恰当的模型进行表示并对其实施计算。工作流要解决的主要问题是：为实现某个业务目标，在多个参与者之间，利用计算机，按某种预定规则自动传递文档、信息或者任务。简单地说，工作流就是一系列相互衔接、自动进行的任务。我们可以将整个业务过程看作是一条河，其中流过的河水就是待审核的表单。

工作流概念起源于生产组织和办公自动化领域，是针对日常工作中具有固定程序活动而提出的一个概念，目的是通过将工作分解成定义良好的任务或角色，按照一定的规则和过程来执行这些任务并对其进行监控，达到提高工作效率、更好的控制过程、增强对客户的服务、有效管理业务流程等目的。尽管工作流从已经取得了相当的成就，但对工作流的定义还没有能够统一和明确，不同学者从不同角度对工作流做出了不同的定义。

三、工作流验证方法的研究现状

1、验证问题及复杂度

工作流过程定义中出现的错误可分为语法错、结构错和语义错。相应地，有语法验证、结构验证和语义验证。语法验证检查过程定义是否符合特定描述语言的语法；结构验证检查过程定义是否会导致错误的执行；而语义验证是层次最高、最完整的验证，保证过程定义与实际业务过程的目标一致性。一般可识别的验证问题及其复杂度如下。

(一)初始化问题:是否存在一个事件序列能引发过程的执行，为NP完全问题。

(二)结束问题:过程是否能够到达结束状态，其求解是指数复杂度的。

(三)死锁问题:各可达状态中是否存在死锁，求解也是指数复杂度的；

(四)活锁问题:各可达状态中是否存在活锁，求解也是指数复杂度的；

(五)迹等价问题:两个过程定义是迹等价的当且仅当它们迹的集合相等，该问题是不可决定的；

(六)安全性问题:过程是安全的当且仅当从各可达状态均可到达结束状态，求解是指数复杂度的；

(七)有界性问题:过程是n一有界的当且仅当在每个可达状态上的执行不超过n次，其求解是多项式完全的。

2验证方法要求

Karamanoli:等人将对工作流过程验证方法的要求总结如下:

(一)需要有坚实的数学基础和严格的形式化分析手段，保证系统的安全性和活性；

(二)需要能在设计时对工作流模型进行详尽的分析和交互仿真；

(三)需要有自动工具支持的算法来有效地计算实现成真实系统后的可用性；

(四)需要有一种综合方法在设计系统时进行渐增式分析，并在多种环境下支持定义重用；

(五)需要产生有意义的、执行路径形式的诊断信息，指出设计中潜在的错误；

(六)对人使用易于理解的图形化表示，为工具提供一套等价的、定义良好的和有效利用空间的形式化符号；

(七)要求没有模拟和形式化方法经验的人也能够理解。合理性验证语言和模型，如Petri网、任务结构、事件驱动的过程链和工作流图等。其中，Petri网是比较突出的具有形式化基础的工具之一，利于完成过程验证。有些方法使用基本Petri网，也有些方法使用Petri网变种，如ICN(information Control net)网、工作流网和其他高级Petri网。使用Petri网进行模拟和验证的主要优点在于:①图形表示清晰直观且表达能力强②具有数学理论基础便于分析。③是可执行的工具，用它描述的系统可以从概念级平滑过渡到实现级，便于仿真。

3验证方法和工具

根据如上定义可知，过程合理性与可达性、活性等概念密不可分。通常，验证合理性所采取的办法是根据过程模型的特点，选取便于验证的几种特性(如安全性、死锁等)，然后根据性质间的因果关系导出合理性。

4化简验证

化简技术也称归约技术或模型转换技术，基本思想为在特性保持的原则下，将过程模型化简为适当规模，以便检测各种冲突。

四、工作流模型的验证

工作流模型的正确执行是提高企业竞争力，改善企业服务质量的关键因素之一。包含逻辑错误的过程模型将导致丢失的货物、顾客的抱怨、利润的失去。过程模型中的一些缺陷也可能产生低的服务质量，并需要额外的修补措施。因而，在工作流模型执行以前，一个重要的要求之一就是能对工作流模型进行分析。总的说来，大概有以下三类分析方法:

1证实(validation)，即测试工作流运行是否和规定的模型一致。

2验证(verifieation)，即证明工作流模型是正确的。

3性能分析，即估算工作流的运行时间、服务质量、资源利用情况是否满足要求。

第一种和第三种方法。即证实(Validat:on)和性能分析，能够通过仿真进行。也就是说，通过一些大量的工作流实例，以检查工作流运行是否能很好地按设计要求完成。而第二种方法，即工作流模型的验证，必须在工作流执行以前，对模型进行形式化的验证，以证明模型能100%的正确。因而，验证的方法更优于证实方法，因为经过验证正确的模型能够确保成功。

而验证问题在大多数商品化工作流产品中并没有涉及到。仅在少数几个研究项目中谈到口。例如。尽管wIDE项目在概念层采用了WFDL语言来描述工作流模型，其实现是基于ECA主动规则。这些规则能够由工作流规范自动或半自动地产生。但它并没有给出其形式化语义，因而，也不可能推理工作流规范的正确性。

Hofstede首先谈到了工作流模型验证的复杂性问题。通过限制模型为无循环和无同步元素，他证明了终止性问题是一个多项式复杂度问题。w。M。Pwallder通过把工作流模型表示成一种Petri网的变种一WF一11et网，从而利用经典Petrl网的性质对工作流模型进行验证。他证明了一个工作流是有效的(S。undness)当且仅当其对应的WF一11et网是活的。并且有界的，从而可以对Petri网的可达图等性质进行验证。此外，Wander也确定了具有“良好结构”的静态结构约束。值得一提的是。在Mentor项目中。工作流的正确性用时态逻辑来表示。而这些正确性主要是执行时的正确性，即动态约束。工作流模型用Stateeh盯ts来表示，而Stateeharts与有限状态自动机密切相关。因而，Melltor项目中采用了SMC(SymbolieModelCheek:ng)来验证工作流的正确性。SMC是ModelCheeking的一种。ModelCheek:ng是比定理证明更有效的一种模型验证方法，它能够验证给定的规范是否满足设计属性。本质上，ModelChecking验证一个给定的有限自动即是否是一个给定的时态逻辑公式的模型。目前，SMC是最有效的ModelCheek，ng方法，它是基于用OBDD紧凑、符号表示有限状态自动机。总之，较之工作流仿真而言，工作流验证更未引起足够的重视。只有少数几个项目对其进行了研究。

五、进一步研究方向

以上我们所介绍的方法都是基于结构验证方面的。由WMFC 工作流过程元模型可以知道, 一个完整的过程模型应该包括控制流、数据流和资源三个要素, 只有完整地检查三维元信息共同作用产生的冲突才能确定一个过程能否真正正确实现其业务目标。所以我们还要对过程模型进行语义验证。文献提出了一种三维的扩展 Petri 网———3DWFN, 并基于该形式化模型总结出化简规则以进行语义验证。与语义验证作用的重要性相比, 目前的研究人员在语义验证方面所进行的研究却存在着很大的空白, 所以今后过程验证的重点将会偏向于语义验证。

六、结束语

通过研究，我们发现工作流过程建模中的形式化验证技术还有待遇进一步的深入探讨，工作流的发展有待于我们对其验证技术的提高，优质的验证技术将会不断的改进工作流的使用特性，从而可以让我们更好的使用工作流。

参考文献

[1]周建涛,史美林,叶新铭.一种基于Petri网化简的工作流过程语义验证方法[J]. 软件学报.2005(07)

[2]李伟,李青.基于J2EE的工作流管理系统框架研究与实现[J].微计算机信息. 2004(08)

[3]赵磊,钱乐秋,赵文耘.基于状态空间的工作流模型验证[J].计算机工程与应用. 2004(10)