（计算机软件与理论专业论文）工作流模型正确性验证问题研究.pdf

山东大学硕士学位论文 工作流模型正确一眭验证问题研究 研究生巩垒 指导教师王海洋教授 摘要 工作流技术已成为当前i t 领域的一个研究热点。目前已经出现了不少工作 流产品和工作流原型系统。工作流模型是业务过程的计算机化的形式表示，工 作流管理建立阶段的功能主要是完成过程建模的任务，不同的工作流管理系统 所实现的工作流模型是各不相同的。对于工作流模型的正确性研究是一个重要 的但是尚未得到很好解决的问题，也就是说，一旦工作流模型建立起来以后， 如何保证它不存在错误的逻辑? 本文首先综述了当前工作流模型及其验证方法，着重介绍了基于p e u i 网进 行工作流建模和验证的优缺点，然后提出了一个基于双分支条件有向图 ( d o u b l e r o a dc o n d i t i o n a ld i r e c t e dg r a p h ( d c d g ) ) 的工作流模型，该模型是一 个工作流实际业务流程的抽象，它建立在状态图和e c a 规则的基础上，具有较 强的表达力和直观的图形描述，同时底层通讯机制基于对象和e c a 规则，便于 进行语义化描述。 工作流模型正确性验证问题是工作流研究领域中的一个重要问题，工作流 管理系统可能建立错误的工作流模型，导致工作流的执行出现异常。有的研究 者将事件平衡分析方法引入了工作流模型，通过分析局部工作流的控制逻辑， 提出了验证工作流控制逻辑正确性的一个必要条件，但是并没有涉及到如何解 决整个工作流的控制逻辑正确性验证问题。本文在基于双分支条件有向图的工 作流模型基础上，提出了一种验证整个工作流控制逻辑正确性的方法，实验结 果表明，该方法是可行的。 工作流管理系统中的时间管理问题是工作流研究领域中另一个重要的问 题，通过对工作流活动加以时间约束，可以保证工作流正确、高效的执行。目 前，许多研究者对工作流模型中时间属性进行建模，进行了一些有益的工作， 但是对于工作流活动时间约束的正确性验证问题和时序逻辑的推理问题没有深 入的讨论。本文首先分析了工作流管理系统中主要应该考虑的时间问题，然后 i 在双分支条件有向图模型基础上进行了一些关于时序逻辑推理问题的研究，提 出了四个推理规则，同时提出了验证工作流活动时间约束正确性的一些必要条 件。研究结果表明，所作的工作对于工作流管理系统的时间建模，监控和性能 评价有一定的参考价值。 另外，本文提出了一个基于对象的工作流活动定义，在此基础上引入了e c a 规则，作为对象消息通讯的基础。在考虑工作流活动之间的控制依赖和数据依 赖的同时，引入了资源依赖的概念，同时提出了强数据依赖、强控制依赖和强 资源依赖的概念，文中给出了关键的消息规则。 最后，我们将本文提出的验证思想用于实际的电子政务软件开发中，分析 设计了正确的业务工作流控制模型和组织模型，进行了有益的尝试。 关键字：工作流正确性控制逻辑时序逻辑e c a 规则 山东大学硕士学位论文 r e s e a r c ho nt h es o u n d n e s sv e r i f i c a t i o n o fw o r k f l o wm o d e l p o s t g r a d u a t e ： g o n gl e i t u t o r ：p r o f w a n gh a i y a n g a b s t r a c t w o r k f l o wh a sb e e nb e c o m i n gah o tt o p i ci ni tr e s e a r c hf i e l d a n dm a n yw o r k f l o w s y s t e m sa n dp r o t o t y p e s h a v eb e e nd e v e l o p e dc u r r e n t l y , w o r k f o wm o d e li st h e p r o c e s sr e p r e s e n t e db yc o m p u t e r o n eo ft h et a s k so fw f m si st oc r e a t et h e w o r k f o wm o d e l s ，a n dd i f f e r e n tw i m s sh a v ec r e a t e dd i f f e r e n tw o r k f i o wm o d e l s p r e s e n t l y ，t h er e s e a r c ho nt h es o u n d n e s so fw o r k f l o wm o d e li sa ni m p o r t a n ta r e ab u t t h eq u e s t i o nh a sn o tb e e nw e l ls o l v e d h o wt oa s s u r et h es o u n d n e s sa f t e raw o r k f l o w m o d e li sc r e a t e d ? i nt h i s t h e s i s ，f r s t l y , w e s u m m a r i z et h e n o w a d a y sw o r k f l o wm o d e l sa n dt h e v e r i f i c a t i o nm e t h o d s ，e m p h a s i z i n go nt h ea d v a n t a g ea n dd i s a d v a n t a g eo fw o r k f l o w m o d e la n dv e r i f i c a t i o nm e t h o db a s e do np e t r in e t ；t h e nw ep r o p o s e daw o r k f l o w m o d e lb a s e do nd o u b l e - r o a dc o n d i t i o n a ld i r e c t e dg r a p h ( d c d g ) ，w h i c hi s a n a b s t r a c tm o d e lo fp r a c t i c a lp r o c e s s e s t h em o d e li sb a s e do ns t a t e c h a r ta n de c a r u l e sa n dh a sas t r o n ge x p r e s s i v ea b i l i t y & i n t u i t i o n i s t i cg r a p hd e s c r i p t i o n a tt h e s a m et i m e ，t h ec o m m u n i c a t i o nm e c h a n i s mi sb a s e do n o b j e c ta n de c a r u l e s ，w h i c h c a nb ed e p i c t e db ys e m a n t i cm e t h o d v e r i f i c a t i o no fw o r k f i o ws o u n d n e s si sa ni m p o r t a n t p r o b l e mi nt h ec u r r e n tw o r k f l o w r e s e a r c ha r e a m a n yw t m s s p r o b a b l yc r e a t ew r o n gw o r k f l o wm o d e l s ，s ot h er u n n i n g o fw o r k f i o ww i l lb ea b n o r m a l s o m er e s e a r c h e r si n t r o d u c et h et h e o r e mo fe v e n t b a l a n c e an e c e s s a r yc o n d i t i o nt ov e r i f yw o r k f l o w l o g i c a ls o u n d n e s si sp r o p o s e db y a n a l y z i n gt h es o u n d n e s so fl o c a lw o r k f l o w b u th o w t o v e r i f yt h es o u n d n e s so fa w h o l ew o r k f l o wi sn o ti n t r o d u c e d i nt h i st h e s i s ，b a s e do nd c d g w o r k f l o wm o d e l a m e t h o dt ov e r i f yt h es o u n d n e s so faw h o l ew o r k f l o wi s p r o p o s e d t h ee x p e r i e n t i a l r e s u l t sp r o v et h a tt b em e t h o di sf e a s i b l e i i i 山东大学硕士学位论文 t i m em a n a g e m e n tp r o b l e mi nw o r k f l o wm a n a g e m e n ts y s t e mi sm o t h e rc r u c i a l p r o b l e m i nw o r k f l o wr e s e a r c ha r e a aw o r k f l o w c a l le x e c u t e c o r r e c t l y a n d e f f e c t i v e l yb ya p p l y i n gt i m ec o n s t r a i n t so nw o r k f i o wa c t i v i t i e s a tp r e s e n t ，m a n y r e s e a r c h e r sm a k et e m p o r a la t t r i b u t e sm o d e l si nw o r k f l o wa n dh a v ed o n eal o to f u s e f u lw o r k ，b u tt h es o u n d n e s sv e r i f i c a t i o no ft e m p o r a la t t r i b u t e si nw o r k f l o wa n d t e m p o r a ll o g i c a li n f e r e n c ep r o b l e mh a v e n o tb e e nd e e p l yr e s e a r c h e d i nt h i st h e s i s ， w e a n a l y z et e m p o r a lp r o b l e m s w h i c hs h o u l d b ec o n s i d e r e di nw o n f l o w m a n a g e m e n t sa n d b a s e do nt h ed c d gw o r k f l o wm o d e lw eh a v ed o n es o m e r e s e a r c h e sa b o u t t e m p o r a ll o g i c a l i n f e r e n c e p r o b l e m a n d g i v e s o m en e c e s s a r y c o n d i t i o n st ov e r i f yt h et e m p o r a lc o n s t r a i n ts o u n d n e s so fw o r k f l o wa c t i v i t i e s t h e r e s e a r c hr e s u l t si n d i c a t et h a tt h e s ew o r ka r eu s e f u l f o r t e m p o r a lm o d e l i n g 、 m o n i t o r i n ga n dp e r f o r m a n c ee v a l u a t i n gi nw o r k f l o wm a n a g e m e n ts y s t e m s ， i na d d i t i o n ，ad e f i n i t i o no fw o r k f l o wa c t i v i t i e sb a s e do n o b j e c ti sp r o p o s e di nt h i s t h e s i s b a s e do r lo b j e c t ，e c ar u l e sa r ei n t r o d u c e d ，w h i c ha c ta st h eb a s i co f c o m m u n i c a t i o n so f o b j e c tm e s s a g e s c o n t r o ld e p e n d e n c y ，d a t ad e p e n d e n c ya n d r e s o u r c ed e p e n d e n c yb e t w e e nw o r k f l o wa c t i v i t i e sa r ec o n s i d e r e d b e s i d e s ，s t r o n g d a t ad e p e n d e n c y ，s t r o n gc o n t r o ld e p e n d e n c ya n d s t r o n gr e s o u r c ed e p e n d e n c y a r e p r o p o s e d t o o i nt h i st h e s i s ，k e ym e s s a g er u l e sa r ed e s c r i b e d a tl a s t ，w ea p p l yt h ev e r i f i c a t i o nt h e o r yi nt h ed e v e l o p m e n to f e _ g o v e r n m e n tm i s t oc r e a t et h es o u n d p r o c e s sw o r k f i o wm o d e la n do r g a n i z a t i o nm o d e l ，a n dh a v ed o n e s o m eu s e f u lr e s e a r c h k e y w o r d s ：w o r k f l o w , s o u n d n e s s ，c o n t r o ll o g i c ，t e m p o r a ll o g i c ，e c ar u l e s v 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独 立进行研究所取得的成果。除文中已经注明引用的内容外，本论文不 包含任何其他个人或集体已经发表或撰写过的科研成果。对本文的研 究作出重要贡献的个人和集体，均己在文中以明确方式标明。本声明 的法律责任由本人承担。 论文作者签名：堑i 垒日期：m 鲁拜阳 关于学位论文使用授权的声明 本人完全了解山东大学有关保留、使用学位论文的规定，同意学 校保留或向国家有关部门或机构送交论文的复印件和电子版，允许论 文被查阅和借阅；本人授权山东大学可以将本学位论文的全部或部分 内容编入有关数据库进行检索，可以采用影印、缩印或其他复制手段 保存论文和汇编本学位论文。 ( 保密论文在解密后应遵守此规定) 论文作者签名：监导师签名：艺蚱日 期：尘堕塑 山东大学硕士学位论文 第一章绪论 1 1 工作流问题的起源与发展 工作流( w o r k f l o w ) 的概念起源于生产和办公自动化领域。通过将一些具有 固定程序的工作分解成定义良好的任务、角色，并且按照预先定义好的规则和 过程来执行这些任务并对执行过程进行监控，从而可以达到提高办事效率、降 低生产成本、提高企业生产经营管理水平和竞争力的目的。 工作流技术的历史可以追溯到上个世纪7 0 年代末的办公自动化和任务批 处理。而第一次使用工作流术语则可以追溯到上世纪8 0 年代初，但是那个时候 还没有真正的工作流管理系统出现。 2 0 世纪8 0 年代中期，f i l e n e t 和v i e w s t a r 等公司率先开拓了工作流产品市 场，成为最早的一批工作流产品供应商。它们把图像扫描、复合文档、结构化 路由( s t r u c t u r e dr o u t i n g ) 、实例跟踪、关键字索引以及光盘存储等功能结合在 一起，形成了一种全面支持某些业务流程的集成化的软件( 包) ，这便是早期的 工作流管理系统。典型的有f i l e n e t 于1 9 8 4 年推出的w o r k f l o 商用系统，v i e w s t a r 于1 9 8 8 年推出的v i e w s t a r ，i b m 于1 9 8 8 年推出的i m a g e p l u s 。这种集成化的软 件系统为企业简化与重组自己的关键业务流程提供了一种非常好的方法。由此 可见，工作流从最初的诞生之曰起就是作为一种面向过程的系统集成技术而出 现的。只不过是限于当时技术水平，它所集成的功能较简单丽已。 进入上个世纪9 0 年代，随着计算机与网络技术的迅速发展，特别是在 i n t e r n e t 应用日益普及的情况下，现代企业信息系统的分布性、异构性和自治性 的特征越来越显著。c s ( 客户端服务器) 体系结构和分布式处理技术( c o r b a 、 d c o m ) 的广泛应用说明集中式信息处理的时代即将成为过去，取而代之的将 是大规模的异构分布式信息处理与应用环境。这种新的处理模式和应用环境要 求应用系统不仅仅要处理单个的任务，还要能够控制、监视和支持处理过程的 逻辑，即实现处理过程的自动化或者半自动化。在这种背景下，工作流管理系 统由最初的无纸化办公环境转而成为在企业复杂信息环境中实现业务流程自动 执行的必要工具。这样的一个转变，把工作流技术带入了一个崭叛的发展阶段， 山东- r 大学硕士学位论文 使得人们从更深层次、更广的领域对工作流展开研究。 目前，在全球范围内。对工作流技术的研究以及相关的产品开发进入了更 为繁荣的阶段，更多更新的技术被集成进来，文件管理系统、数据库、电子邮 件、移动式计算、网格计算、i n t e r n e t 服务等都己经被容纳到工作流管理系统中 来。同时，工作流产品的市场也得到了很大的发展。目前市场上具有代表性的 工作流产品有：i b m 的m q s e r i e sw o r k f l o w 、a c t i o n 技术公司的m e t r o 、f i l e n e t 公司的v i s u a lw o r k f l o 、j e t f o r m 公司的i n t e m p o 和p a v o n e 公司的e s p r e s s o 等。 1 。2 工作流管理系统的基本概念和参考模型 1 9 9 3 年工作流管理联盟( w o r k f l o w m a n a g e m e n tc o a l i t i o n ，w f m c ) 的成立 标志着工作流技术丌始进入了相对成熟的阶段。为了实现不同工作流产品之间 的互操作性，w f m c 在工作流的相关术语、体系结构以及应用编程接口( w a p i ) 等方面制定了一系列标准。 根据工作流联盟( w f m c ) 的相关文件i2 1 ，工作流和工作流管理系统的定义如 下： 工作流：工作流是一类能够完全或者部分自动执行的经营过程，在工作流 中，文档、信息或任务按照一定的程序规则在参与者之问传递，以完成相应工作。 工作流管理系统( w f m s ) ：是一种能定义、创建和管理工作流执行的系统。 它可通过一个或多个工作流机来运行，并能解释过程定义、与工作流参与者交互， 在需要时还可以引用i t 工具和应用。通常，工作流管理系统是指运行在一个或 者多个称为工作流机的用于定义、实现和管理工作流运行的一套软件系统，它 和工作流执行者交互，推进工作流实例的执行，并监控工作流的运行状态。在 工作流管理系统的支撑下，通过集成具体的业务应用软件和操作人员的界面操 作，才能够良好地完成对企业经营过程运行的支持。 为了便于工作流管理系统的研究与开发，w f m c 提出了一个工作流系统参 考模型，其体系结构、主要组成部分和接口如图1 1 所示。 丽 l 控硼l 1 一 图1 一l 工作漉系统参考模型 工作流执行服务( w o r k f l o we n a c t m e n ts e r v i c e ) 是参考模型的核心部分，围 绕它的外部接口包括工作流应用程序接e l ( w a p i ) 和交换格式等。通过这些接 口可以访问工作流系统服务，并控制工作流控制软件与其它的系统组件之间的 交互。w a p i 是一个统一的服务接口，根掘不同的功能范围分为五个接口，如 图1 1 所示。 该参考模型在逻辑上把过程、活动控制逻辑与应用工具和最终参与者端的 任务分开。这样使得制订广泛的工业标准，或者将参与者专用的应用工具集成 到特殊的工作流应用程序中变得可能。 1 3 工作流管理系统的分类 根据所实现的业务过程，工作流管理系统可以分为四类： ( 1 ) 管理型工作流( a d m i n i s t r a t i v ew o r k f l o w ) ：在这类工作流中，活动可以预定 义并且有一套简单的任务协调规则，例如项目申请审批流程。 ( 2 ) 设定型工作流( a d h o cw o r k f l o w ) ：与管理型工作流类似，但一般用来处理 异常或发生机会比较小的情况，有时甚至是只出现一次的情况，这与参与 的用户有关。 ( 3 ) 协作型工作流( c o l l a b o r a t i v ew o r k f l o w ) ：参与者和协作的次数较多。在一个 步骤上可能反复发生几次直到得到某种结果，甚至可能返回到前一阶段， 参见文献 3 。 ( 4 ) 生产型工作流( p r o d u c t i o nw o r k f l o w ) ：实现重要的业务过程的工作流，特别 是与业务组织的功能直接相关的工作流。与管理型工作流相比，生产型工 山东大学硕士学位论文 作流一般应用在大规模、复杂的和异构的环境下，整个过程会涉及许多人 和不同的组织。 根据底层实现技术，工作流管理系统分为三类： ( 1 ) 以通讯为中一t 2 , ：以电子邮件为底层的通讯机制。这种类型的工作流管理系 统适合于协作型和不确定型工作流，而不适于生产型工作流。 ( 2 ) 以文档为中心：基于文档流转的思想，与外界应用交互有限。由于管理型 工作流很多都是基于表单处理的，可以用以文档为中心的工作流管理系统 实现，适应于电子政务工作流。缺点是系统不能主动的把任务提供给用户， 往往依赖用户连接并注册到w e b 服务器上。 ( 3 ) 以过程为中心：对应予生产工作流，它实现自己的通讯机制，在底层数据库基 础上，提供大量与新老应用系统交互的接口。 1 4 工作流建模方法及正确性验证方法研究现状 工作流模型是业务过程的计算机化的形式表示。工作流管理建立阶段的功 能主要是完成过程建模的任务。不同的工作流管理系统所实现的工作流模型是 各不相同的：工作流正确性验证有其重要的意义，由于工作流管理系统可能会 建立错误的工作流模型，从而会导致工作流的执行出现异常，因此，建立工作 流模型的同时，必须考虑其是否正确。目前，主要的建模方法有以下几种： ( 1 ) 基于脚本语言的建模方法 脚本语言中有描述控制流和数据流的语句结构，它提供了种简明的描述 方法，对于有经验的设计者来说更易于使用。它的主要缺点是缺乏流程本身的 形式化语义，同时并没有很好的方法对建立的工作流模型进行正确性验证。 ( 2 ) 基于网的建模方法 适合于流程的可视化建模，一般都使用状态变迁网，流程中的活动用结点 表示，控制流用边表示。使用状态变迁网的主要问题在于是否有形式化的语义， 大多数工作流产品的可视化建模方法都缺乏形式化语义。在具有形式化语义的 状态变迁网中，使用的最多的就是p e t r i 网和状态图( s t a t ec h a r t s ) 。具有形式 化语义的基本网的方法可以转换成其它建模方法，如基于规则的、时序逻辑的 和脚本语言的方法等。传统的p e t r i 网具有直观的图形表示、明确的语义、丰富 的分析技术等，但它不能完全描述任务间的条件关系，不能表示外部事件及时 序对工作流程的干预( 即开放性) ，并且不支持动态性，而这些在应用中又是不 坐奎盔兰堡圭堂垡丝塞 可避免的。文献4 提出了基于p e t r i 网的分析方法，通过某些限制提出了一个可 以在多项式时间内验证正确性的模型结构w f n e t 。但由于模型本身所具有的描 述能力上距离对工作流过程本质的描述仍有差距，所以模型本身表达力具有一 定的局限性。 ( 3 ) 基于规则的建模方法1 5 1 目前研究的较多的是基于e c a 规则的建模。e c a ( e v e n t - c o n d i t i o n a c t i o n ) 规则具有形式化基础，也可以转换成其它的建模方法，如p e t r i 网、时序逻辑等， 但是e c a 规则的可视化工作量比较大。 在m e t e o r 项目中，类似于e c a 的规则用来表示任务间的状态和值依赖 关系。状态依赖规定了一个可控制任务变迁如何依赖于其它任务的可观察状态。 事件是隐含的，表示任务变迁到某个状态。规则中的条件可能是任务输出数据、 工作流全局变量的表达式。根据规则，一个任务迁移到另一个新的任务，同时 相应的任务状态发生变化。 在w i d e 中，e c a 规则用来描述由时态事件、工作流内部事件和外部事件 引发的工作流例外处理。工作流内部事件指的是工作流变量更改、约束违例、 任务的取消或者拒绝、执行实体的不可用等。条件可能是有关工作流模型产量 或产品数据的表达式，也可以是时态表达式。动作可以是任务状态修改、例外 处理例程。 e c a 规则不仅能够描述工作流模型中活动之间的协调关系，而且能够表达 组织、角色之间的约束关系。此外。基于规则的方法能够支持过程的动态修改， 角色的调整等，因而使模型具有定的灵活性，能够描述a d h o c 类型的工作流 模型。但e c a 规则作为一种底层实现机制，缺乏图示化的手段和结构化构造工 作流模型的方法。另外，当规则急剧增加时，对规则的处理将是一个很繁琐的 任务。e c a 规则也缺乏逐步求精的手段，就语言而言，e c a 规则本身必须就借 助于其它方法来表示，如上面提到的p e t r i 网和时序逻辑。因此，很难对e c a 规则表示的工作流模型进行形式化的验证。 ( 4 ) 基于逻辑的建模方法 基于逻辑的方法适合于描述系统的动态性，其中时序逻辑是一种常用的方 法，它具有很好的形式化基础，验证工作流模型的属性比较方便。但是时序逻 辑的主要缺点是很难实现可视化，不容易转换成其它的描述方法，描述业务流 程的系统行为太复杂。例如d a v u l c u 采用的并发事务逻辑c t r ( c o n c u r r e n t t r a n s i t i o nl o g i n ) 来表示工作流模型。在c t r 中，在经典的逻辑符号( 与、或、 取反等) 的基础上进行了扩展，引入了新的逻辑连接符号，如并发、可能和单 独执行。与基于图的方法相比，采用逻辑的一个优点是，能够表达全局约束， 这些全局约束也能够用逻辑来刻画，从而使工作流模型的描述和验证在一个统 一的框架中进行。但是，同样由于其设计上难度和缺乏方便的图示化手段，该 方法并没有广泛应用。 ( 5 ) 基于事务模型的建模方法【6 1 事务的概念来源于数据库研究领域，用于解决数据的并发访问和出错恢复 问题。事务性在工作流管理系统中更为重要，因为工作流活动的持续时间有时 很长，工作流执行过程中出现错误的可能性更大。因此，从提高工作流管理系 统的可靠性出发，建立基于事务的工作流具有很重要的意义。在数据库事务模 型基础上，研究人员提出了许多高级事务模型，包括嵌套事务类型( n e s t e d t r a n s a c t i o n ) 7 1 开放嵌套事务模型( o p e n n e s t e d t r a n s a c t i o n ) 【8 】、s a g a ；膜型t 9 1 、 分布式事务管理模型( d i s t r i b u t e dt r a n s a c t i o nm a n a g e m e n tm o d e l ) 以及柔性 事务模型( f l e x i b l et r a n s a c t i o nm o d e l ) “】等。 ( 6 ) 基于代数的方法 进程代数是一种刻画并发计算的一种工具，目前在工作流研究领域中还没 有得到广泛的研究和足够的重视。有的研究人员采用l o t o s 来进行软件过程的 建模。l o t o s 是一种描述通信的进程代数。由于软件过程和业务过程的相似性， 进程代数也可以用来描述工作流模型。同基于逻辑的建模方法一样，进程代数 的方法具有严格定义的形式化语义，容易验证，但缺点是缺乏图示化的手段。 总之，目前的工作流产品中采用p e t r i 网和e c a 规则的方法比较多，p e t r i n 具有图示化的手段和严格的语义定义，能够对建立的工作流模型进行形式化分 析和验证，因而被广泛采用。但p e t r i 的缺点也很明显：图形过于复杂，节点过 多，从而导致普通用户难以掌握。而e c a 规则的方法是种较为理想的底层方 式，但缺乏图示化的手段和逐步求精的手段。 工作流模型的正确执行是提高企业竞争力，改善企业服务的质量的关键因 素之一。如何对工作流进行建模同时对模型的正确 生( s o u n d n e s s ) 进行验证是当 今工作流研究的一个热点，文献 1 2 引入了正确性( s o u n d n e s sp r o p e r t y ) 的概念， 一个工作流是正确( s o u n d ) 的，当且仅当对于任何工作流实例，处理过程都能 够正确的终止。如果过程模型中存在错误的逻辑，会导致严重的后果，并且需 要额外的补救措施。因而，在工作流模型正式运行之前，必须对工作流模型进 行分析。目前，主要的思路有三种： ( 1 ) 证实( - v a l i d a t i o n ) ，通过工作流仿真执行，判断是否和规定的模型一致； ( 2 ) 性能分析( p e r f o r m a n c e a n a l y s i s ) ，也是通过工作流仿真执行，分析工作 流的运行时间、服务质量和资源利用情况； ( 3 )正确性验证( s o u n d n e s sv e r i f i c a l i o n ) ，证明工作流模型是正确的，或者 说不存在错误的逻辑。 前两种方法，需要设计大量的工作流实例，来检查工作流运行是否正常， 而第三种方法，则是在工作流执行之前，对模型进行形式化的验证。因而，从 代价的角度讲，验证的方法优于前两种方法。但是，验证问题在大多数商品化 工作流产品中并没有涉及到。 h o f s t e d e 首先谈到了工作流模型验证的复杂性问题，通过限制模型为无循 环和无同步元素，证明了终止性问题是个多项式复杂度问题。而w m p v a nd e r a a l s t 通过把工作流表示成一种p e t r i 网的扩展：w f n e t ，从而利用经典p e t r i 网 理论对工作流模型进行了验证，证明了一个工作流是正确的当且仅当w f n e t 是活的，有界的，并且是可达的。同时他还提出了一些静态的限制，如自由选 择( f r e ec h o i c e ) 和好的结构( w e l ls t r u c t u r e ) ，但是这种基于p e t r i 网的方法并 没有考虑每个特定任务的语义。 综上所述，一个比较理想的工作流建模方法应该满足下面的条件： ( 1 ) 具有图示化的建模界面，建模用户容易掌握； ( 2 ) 建摸方法或者语言本身是可执行的，可以作为工作流引擎的实现机制，例 如，一般基于规则的方法都可以作为底层实现机制； ( 3 ) 有形式化的语义，也就是说，其语义可以用p e t r i 网、逻辑或者代数表示， 从而可以对模型进行验证和推理。 当今工作流建模的研究有一种混和的趋势：高层面向用户的客户端用图示 化的建模手段，而在底层采用一种或者多种便于实现或者具有严格语义、便于 验证的方法，从而可以将高层描述方法转化为底层方法，便于验证模型和程序 实现。 1 5 本文所做的工作 上文列举了各种主要的工作流建模方法和相应验证方法存在的问题，并提 7 出了理想的工作流建模方法满足的条件。在此基础上，本文主要作了以下研究 工作： ( 1 ) 建立了一个基于双分支条件有向图的工作流模型，该模型是工作流控制 模型的一个抽象，提出了一种验证整个工作流的控制逻辑正确性的算法； ( 2 ) 同时在该模型基础上进行了一些关于时序逻辑推理问题的研究，给出了 验证工作流活动时间约束正确性的一些必要条件以及时序逻辑推理规 则； ( 3 ) 将对象和e c a 规则引入了本文建立的工作流模型，作为底层通讯的机制， 在考虑工作流活动之间的控制依赖和数据依赖的同时，引入了资源依赖 的概念，同时提出了强数据依赖、强控制依赖和强资源依赖的概念，文 中给出了关键的消息规则； ( 4 ) 实践中，我们将本文提出的工作流建模和验证方法应用到山东省民政厅 城市居民最低生活保障电子政务系统设计和开发中，实践证明，该方法 是可行的。本人作为主要人员完成了系统的业务逻辑设计和程序开发工 作。 1 6 本文的组织结构 结合本文所做的研究工作，整篇论文的章节是这样组织的。第一章为绪论 部分，介绍了工作流的起源、发展和基本概念，以及工作流管理系统的分类， 综述了工作流建模和验证方法，介绍了本文所作的主要工作；第二章介绍了p e t r i 网的知识和基于p e t r i 网的工作流建模和验证的方法；第三章建立了一个双分支 条件有向图( d c d g ) 工作流模型；第四章在d c d g 工作流模型基础上，提出 了一个验证工作流正确性的方法：第五章在d c d g 工作流模型的基础上进行了 一些关于时序逻辑推理问题的研究，给出了验证工作流活动时间约束正确性的 一些必要条件；第六章在考虑工作流活动之间的控制依赖和数据依赖的同时， 引入了资源依赖的概念，同时提出了强数据依赖、强控制依赖和强资源依赖的 概念，并且给出了关键的消息规则；第七章介绍了一个电子政务工作流实例， 并将上文提到的建模和验证方法用于业务工作流的设计和开发中；第八章为全 文的结束语。 一垒璧堡些垒垡_ 一 第二章基于p e t r i 网的工作流建模方法 2 1 引言 p e t r i 网是由德国的c a r la d a mp e t r i 于1 9 6 2 年首先提出的，它在博士论文 “c o m m u n i c a t i o nw i t ha u t o m a t a ”首创性地用p e t r i 网描述通信系统，经过近四 十年的发展，它已经成为具有严密的数学基础，多种抽象层次的通用网络，并 在自动控制和计算机科学中得到了广泛应用，如计算机网络的性能分析、并行 程序的设计与分析、系统可靠性分析、分布式计算机系统的分析与控制、软件 工程、知识推理、人工神经元网络和决策模型等领域。与传统的系统建模、分 析和控制方法相比，p e t r i 网作为一种图形化和数学化的建模工具，能够提供一 个集成的建模、分析和控制环境，为系统的设计提供便利。 本章介绍了p e t r i 网的基本概念以及基于p e t r i 网进行工作流建模和验证的 方法。 2 2p e t r i 网的基本概念 定义：p e t r i 网可以用一个三元组表示p n = ( p ，t ，f ) ，其中： p = ( p i ，p 2 ，p 。) ，一个有限的库所( p l a c e ) 集合； t = t 】，t 2 ，t n ，一个有限的变迁( t r a n s i t i o n ) 集合； f ( p t ) u ( t x p ) ，弧( a r c ) 的集合：并且满足下面的条件： ( 1 ) 库所和变迁是两类不同的元素，即p n t = 中； ( 2 ) 另外库所和变迁中至少有一个元素，即put 巾； ( 3 ) k ( p t ) u ( t p ) 是有向弧集，它表示p n 中的流关系： ( 4 ) d o r a ( f ) u c o d ( f ) = p u t ，其中d o r a ( f ) = x 1 3 y ( x ，y ) e f ，c o d ( f ) = y t k ( x ，y ) f ) ，分别为f 的定义域和值域。每个库所代表一种资源，资源的流 动由流关系决定，所以变迁只能与库所有直接的流关系。不参与任何变迁的资 源表现为孤立库所。不引起资源流动的变迁表现为孤立变迁。该条件表示p n 中不能有孤立元素，即孤岛。 库所p 称为变迁t 的输入库所( i n p u tp l a c e ) 当且仅当有一条有向弧从p 到 山东大学硕士学位论文 t ，p 称为变迁t 的输出库所( o u t p u t p l a c e ) 当且仅当有一条有向弧从t 到p 。我 们用t 表示变迁t 的输入库所集，t 表示变迁t 的输出库所集。同理p 表示 共享p 作为输出的变迁集，p 表示共享p 作为输入的变迁集，这里表示托肯 ( t o k e n ) 。 在p e t r i 网的流动过程中，t o k e n 的数量和分布状态是会改变的。我们把 t o k e n 在p e t r i 网中的分布称为p e t r i 网的一个状态。变迁是p e t r i 网中的活动部 件，当一个变迁t 的输入库所集合中每一个库所都至少含有一个t o k e n 时，我 们称变迁t 被授权( e n a b l e d ) 。一个被授权的变迁可以点火或者发生( f i r e o c c u r ) 。 如果变迁t 发生，那么t 消耗它的每个输入库所p 中的一个托肯，并且在它的 每个输出库所p 中产生一个托肯。这样变迁t 的发生就引起了p e t r i 网状态的改 变。 2 3 p e t r i 网模型的基本特性 针对p e t r i 模型，利用可达树、可达图、状态方程和计算机仿真等方法，可 分析p e t r i 网的有界性、活性、周期性等特性。下面列出p e t r i 网的各种特性所 代表的系统特性： ( 1 ) 可达性 可达性是指系统运行过程中能达到指定的状态。状态m l 从状态m 可达， 是指存在有关变迁发生序列6 ，使得m 5 】_ m l 。 ( 2 ) 有界性( 安全性) 有界性反映系统运行过程中对资源变量的需求。在理论分析时常可假定位 置容量为无穷。但在实际系统设计中，必须使网络中的每个位置在任何状态下 的标志数小于位置的容量，这样才能保证系统的正常运行，不至于产生溢出现 象。 ( 3 ) 活性 活性表明系统能正常运行，即无死锁。此特性在系统设计中很重要，要保 证系统避免死锁。 ( 4 ) 回复性 回复性表明系统运行的周期性或循环性。 ( 5 ) 公平性 公平性反映系统的无饥饿性，即系统的各个子部分在竞争共享资源时不出 山东大学硕士学位论文 现饥饿现象。 ( 6 ) 可逆性 可逆性表明系统运行的可恢复性。 ( 7 ) 保守性 保守性表明在实际系统中的资源是受限的，即保守的。 ( 8 ) 一致性 一致性对并行系统和并行算法比较重要，表明系统的两个行为之间不存在 冲突。 2 4p e t ri 网的缺点 p e t r i 网已经广泛地用于系统的描述和分析中，它理论严密，分析方法丰富 有效，在描述同步、资源共享、复杂系统的逻辑关系等方面有很大的优势，可 用于通信协议分析、分布式系统、嵌入式系统、自动生产系统、工作流分析等 方面。然而，p e t r i 网用来描述系统时，也存在些困难。 首先，p e t r i 网本身完全用结构描述问题，没有数据的概念，所有的数据控 制都必须转化成网结构，因此，对某些问题而言，尽管理论上是可以描述的， 但是工程实现上却是非常困难的。 其次，p e t r i 网中没有层次化的设计思想，所有的元素都在一个平面上，建 立的系统模型层次不清，不能与系统本身对应，模型理解困难，维护工作量大， 可重用性差。 第三，p e t r i 网只描述了系统的逻辑结构相关性，没有给出时间上的相关性， 无法描述系统内的时序关系，反映系统有关时间的行为。 第四，p e t r i 网的描述手段过于简单，很多系统内的结构用它描述起来非常 复杂，这在一定程度上限制了它的使用。 2 5 基于p e t ri 网的工作流模型正确性验证 由于p e t r i 网严格的数学基础和图形化的规范语义，对于工作流的建模与分 析的研究人员来讲有很大的诱惑力。 在p e t r i 网的基础上，a a l s t 提出了工作流网( w f n e t ) 的概念，一个p e t r i 网p n