（计算机科学与技术专业论文）面向语义约束的协同验证研究.pdf

在学期间研究成果使用承诺书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：内蒙古大学有权将 学位论文的全部内容或部分保留并向国家有关机构、部门送交学位论文的复印件和磁盘，允 许编入有关数据库进行检索，也可以采用影印、缩印或其他复制手段保存、汇编学位论文。 为保护学院和导师的知识产权，作者在学期间取得的研究成果( 含计算机软件、程序) 属于 内蒙古大学计算机学院。作者今后使用涉及在学期间主要研究内容或研究成果，须征得内 蒙古大学计算机学院就读期间导师的同意；若用于发表论文，版权单位必须署名为内蒙古大 学计算机学院方可投稿或公开发表。 学位论文作者签名： 日 期： 指导教师签名： 日 肭荔 内蒙古火学硕十学位论文 面向语义约束的协同验证研究 摘要 随着网格技术的不断发展及网格应用研究的深入，网格环境下业务流程越 来越复杂。随着业务流程规模因跨领域跨组织而增大，导致业务流程的高复杂 性，就会由于状态空间爆炸而给网格工作流的验证带来困难。本文针对这个问 题，研究面向语义约束的协同验证方法，使协同验证基于化简技术，提高验证 效率。主要做了以下几个方面的工作： ( 1 ) 研究协同验证的概念和模型。深入分析了网格工作流验证的研究现状， 突破已有研究中结构验证的局限，研究协同验证的理论，建立理论模型，提出 了协同验证具有二维性的观点。 ( 2 ) 研究协同验证过程。已有研究中的验证都不具有分布式特性，而协同验 证是分布式的。考虑子模型之间存在的关系，定义了s c n 的协作方式，分析了 合成模型的验证方法。论证了协同验证在两个维度上交叉验证的合理性，并比 较了交叉验证与“先子模型，后合成 验证方法的区别，说明了协同验证具有 动态性的优势。 ( 3 ) 研究协同验证的化简规则。结构化简的原则是无结构冲突，不适用于协 同验证。协同验证的化简规则是在语义约束一致性的原则下，逐步规约模型中 无语义冲突的部分。根据网结构的不同，基于s c n 提出一组子网级化简规则， 证明了这组化简规则的活性保持性、有效性和完备性。以网上购物流程为例， 说明了上述方法的有效性。 关键词：协同验证，语义约束，化简，网格工作流，p e t r i 网 o nv e r i f i c a t i o ni nt h ee x i s t i n gr e s e a r c h ，b u tc o v e r i f i c a t i o ni s c o n s i d e r i n gt h e? r e l a t i o n s h i pb e t w e e ns u b m o d e l s ，t h ec o o p e r a t i v ea p p r o a c h e sb a s e do ns c n h a v e b e e ng i v e n ，t h ev e r i f i c a t i o no ns y n t h e s i sm o d e lh a sb e e na n a l y z e d ，a n dt h er e a s o n a b l e o fc r o s s v a l i d a t i o np r o c e s sh a sb e e np r o v e d t h ec o - v e r i f i c a t i o nw h i c hh a st h e a d v a n t a g eo fd y n a m i ch a sb e e ni l l u s t r a t e dt h r o u g hc o m p a r i n gc r o s s v a l i d a t i o nw i t h f i r s ts u b m o d e l ，t h e nt h es y n t h e s i sm o d e l m e t h o d ( 3 ) r e s e a r c ho nt h er e d u c t i o nr u l e so fc o - v e r i f i c a t i o n t h ep r i n c i p l ei ns t r u c t u r e l l i 内蒙古大学硕十学位论文 v e r i f i c a t i o ni sn os t r u c t u r ec o n f l i c t s ，b u ti td o e sn o ta p p l yt oc o v e r i f i c a t i o n t h e r e d u c t i o nr u l e si nc o - v e r i f i c a t i o ns e et h ec o n s i s t e n c yi ns e m a n t i cc o n s t r a i n t sa s p r i n c i p l e ，r e d u c i n gt h em o d e lw h e nt h e r e a r en os e m a n t i cc o n f l i c t s g r a d u a l l y a c c o r d i n g t od i f f e r e n tn e t w o r ks t r u c t u r e ，as u b n e tl e v e lr e d u c t i o nr u l e sh a sb e e np u t f o r w a r db a s e do ns c na n dt h el i v e n e s s ，e f f e c t i v e n e s sa n d c o m p l e t e n e s so f t h e s er u l e s h a v eb e e nd e m o n s t r a t e d a ni n s t a n c eo fs h o p p i n go n l i n ei sg i v e nt o i l l u s t r a t et h e a v a i l a b i l i t yo ft h et e c h n i q u e sd e s c r i b e da b o v e k e y w o r d s ：c o v e r i f i c a t i o n ，s e m a n t i cc o n s t r a i n t ，r e d u c t i o n ，g r i dw o r k f l o w , p e t r i n e t l l i 面向语义约束的协同验证研究 目录 摘要i a b s t r a c t i i 第一章绪论1 1 1 引言1 1 2 工作流技术l 1 2 1c s c w 和工作流技术2 1 2 2 网格工作流的概念。2 1 3 工作流的验证3 1 3 1 网格工作流验证的研究现状4 1 3 2 网格工作流验证中存在的问题。5 1 4 有关本论文6 1 4 1 主要研究内容6 1 4 2 主要贡献和创新点。7 1 4 3 论文结构安排7 第二章网格工作流的协同验证理论9 2 1c s c n 的基本概念9 2 1 1p e t r i 网的基本概念。9 2 1 2 语义约束网s c n 1 0 2 1 3s c n 的协作方式1 1 2 2 协同验证的概念和模型1 4 2 2 1 协同验证的概念1 4 2 2 2 协同验证的过程1 6 2 2 3 大规模复杂流程协同验证的特点1 8 2 3 本章小结1 9 第三章网格工作流协同验证的化简规则。2 0 3 1 协同验证的化简规则2 0 i v 内蒙古大学硕十学位论文 3 1 1 子网类型定义2 0 3 1 2 子网级化简验证的前提2 5 3 1 3 子网级化简规则描述2 6 3 1 4 子网化简的活性保持性4 0 3 2 化简规则有效性与完备性的证明。4 1 3 3 示例。4 2 3 4 本章小结4 4 第四章应用实例。4 5 4 1 实例描述4 5 4 2 子模型的建立4 5 4 2 1 客户流程4 5 4 2 2 商家流程4 6 4 2 3 邮局流程4 7 4 2 4 银行流程4 8 4 4 子模型的化简。4 9 4 4 合成模型的化简。5 1 4 5 本章小结5 3 第五章结论和进一步的工作5 5 5 1 论文总结。5 5 5 2 进一步的工作。5 5 参考文献5 7 致谢6 l 附：攻读硕士期间参加的研究项目6 2 v 面向语义约束的协同验证研究 图表目录 图2 i 子网顺序协作方式示意图 图2 2 与分支协作方式的子网合成示意图 图2 3 子网与分支协作方式示意图图2 4 子网与合并协作方式示意图 图2 5 子网或分支协作方式示意图图2 6 子网或合并协作方式示意图 图2 7 子网异或分支协作方式示意图图2 8 子网异或合并协作方式示意 图2 9 协同验证模型图1 8 图3 1s c n - 子网的类型2 2 图3 2 无输入无输出p p 型子网化简过程2 7 图3 3 单输入单输出p p 型子网化简过程2 8 图3 4 单输入异或输出p p 型子网化简过程2 9 图3 5 多输入多输出p p 型子网化简过程3 0 图3 6p 。，e o 中库所都唯一的t t 型子网化简过程3 1 图3 7p 。中库所唯一，p o 中库所表现为“与 语义的t t 型子网化简过程3 1 图3 8p 。中库所唯一，p 。中库所表现为“或 语义t t 型子网化简过程3 1 图3 9p ，中库所表现“与语义，p o 中库所唯一的t t 型子网化简过程3 2 图3 1 0p 。中库所表现为“或”语义，p o 中库所唯一t t 型子网化简过程3 2 图3 1 lp 。，p o 中库所表现为“与”语义t t 型子网化简过程3 3 图3 1 2p 。中库所表现为“与 语义，p 0 中库所表现为“或 语义t t 型子网化简过程3 3 图3 1 3p 。中库所表现为“或 语义，p o 中库所表现为“与”语义t t 型子网化简过程3 3 图3 1 4p 。中库所表现为“或 语义，p 0 中库所表现为“或”语义t t 型子网化简过程3 4 图3 1 5 阢单输入，p 0 中库所唯一p t 型子网化简过程3 5 图3 1 6p 。单输入，p o 中库所表现为“与 语义p ，r 型子网化简过程3 6 图3 1 7p ；单输入，p 0 中库所表现为“或语义p t 型子网化简过程3 6 图3 1 8p ，与输入，p 。中库所唯一p t 型子网化简过程3 6 图3 1 9p 中库所唯一，p 。单输出t p 型子网化简过程3 8 图3 2 0p 。中包含表现为与语义，p o 单输出t p 型子网化简过程3 9 图3 2 1p 。中包含表现为或语义，p o 单输出t p 型子网化简过程3 9 v l 内蒙古大学硕士学位论文 图3 2 2 火车订票流程图4 3 图3 2 3 火车订票流程图化简示意图4 3 图4 1 客户流程4 6 图4 2 商家流程4 7 图4 3 邮局流程4 8 图4 4 银行流程4 9 图4 5 客户流程化简过程5 0 图4 6 银行流程化简过程5 0 图4 7 网上购物流程5 l 图4 8 化简过程示意图5 3 v i i 面向语义约束的协同验证研究 为继 、数 同服 务平台。网格技术的兴起为解决协同服务的集成提供了新的方法和实现途径。 从网格的起源和目的看【3 】，网格的本质是“资源共享与协同工作 。网格的目的是利用互 联网把分散在不同地理位置的电脑组织成一台“虚拟的超级计算机 ，实现计算资源、存储资 源、数据资源、信息资源、软件资源、通信资源、知识资源、专家资源等全面的资源共享。 为了灵活有效地组织网格上的资源，将网格上的资源以及网格的功能以网格服务的形式进行 组织。并将网格环境下不同的网格服务按照一定方式组织起来，形成一个新的组合网格服务， 使得用户能够像使用普通网格服务一样使用该组合网格服务，从而达到解决复杂问题的目的。 网格环境中的各种网格服务在网格的各节点间串行或并行执行【4 j ，协同的完成企业( 或 组织) 的业务流程，达到组织内部或组织之间的资源共享并提高工作效率。对于网格的研究 和应用，不仅需要利用网格实现资源共享，而且需要在这些资源的基础上开展协同工作，使 网格应用能够自动或者半自动执行，尤其当网格应用的逻辑过程比较复杂，具有各种时间和 因果约束的时候，更需要有相应的服务和技术束管理这些应用。因此，网格工作流随着网格 研究的深入而得到了重视。 网格工作流【5 】是一个网格服务自动化处理的过程，它根据一系列的过程规则，能够完全 、或部分地把运行在网格环境下的各种互相作用的网格服务有机地结合在一起，其间的信息或 数据在不同的网格服务之间传递和执行。网格工作流是一种有效的网格业务建模和网格资源 整合技术，也是传统工作流技术在网格环境中的一个应用，尚待进一步发展和完善。 1 2 工作流技术 工作流技术是计算机技术应用的一个重要方面，也是并行工程实施过程中的一项重要的 技术。工作流技术主要是利用计算机科学技术，结合企业具体产品开发过程与经营管理进行 面向语义约束的协同验证研究 信息化软件系统的应用开发，达到企业经营和生产过程全自动或半自动化的执行和管理【6 1 。 工作流技术不仅是- n 计算机应用技术，也是一个涉及多学科交叉的研究领域。 1 2 1c s c w 和工作流技术 计算机技术的发展把人类社会带入了信息化时代，随着信息化进程的深入，通信技术与 计算机及其网络技术相融合，产生了一个新的研究领域计算机支持的协同工作c s c w ( c o m p m e rs u p p o r t e dc o o p e r a t i v ew o r k ) 【7 1 。c s c w 是一个多学科交叉的研究领域，它的目标是 利用计算机技术和网络技术的最新研究成果来满足人类工作中对群体性、协作性的要求。 根据w f m c 的定义，工作流就是自动运作的业务过程的部分或整体，表现为参与者对文 件、信息或任务按照规程采取行动并令其在参与者之间传递【8 】。由于工作流技术能够使过程 自动化和协同工作，提高工作效率，因此在企业的业务流程重组、电子商务、协同科学研究 领域受到了广泛的重视。它提出的目的是通过将工作分解成定义良好的任务、角色，按照一 定的规则和过程来执行这些任务并对它们进行监控，达到提高办事效率，降低生产成本、提 高企业生产经营管理水平和企业竞争力的目标。 然而，在以往的协同工作中没有对工作流程的管理和控制，因此无法支持完整的办公和 业务处理过程，为了适应迅速变化的市场，快速响应企业的各种需求，需要重新定制工作流 程，充分合理地利用企业各类资源，实现业务处理过程的自动化，无纸化及全球化，从而提 高工作效率和质量，加快反应速度，降低办公费用。作为计算机支持的协同工作c s c w 研究 的一个重要方向，工作流技术是实现上述思想的关键技术，从而引起了研究机构与产业界的 广泛关注。 1 2 2 网格工作流的概念 围绕着工作流的过程建模、组织建模、资源建模、执行调度、监控管理、模拟分析、互 操作、柔性适应性，工作流研究取得了很多研究成果。网格工作流借鉴了传统工作流的思想， 因此网格工作流和传统工作流有许多相同点。网格工作流与传统工作流一样包含四个基本要 素：工作流模型、工作流运行机制、人和外部程序。 然而在网格环境下可能需要处理动态资源信息、复杂组织、多种策略和选择等问题。网 格的特点使得传统工作流不能够在网格环境很好的工作，或者根本不适用。也就是说，网格 工作流与传统工作流相比存在很多的不同点。主要包括以下几个方面： ( 1 ) 网格工作流是基于虚拟组织的工作方式，虚拟组织是松耦合的，包括多个管理领域 2 内蒙古大学硕士学位论文 和组织，缺乏集中的控制。 ( 2 ) 网格工作流是基于网格服务的应用方式，根据o g s a 规范，采用一致的网格服务方 式来处理各种应用，有效的解决异构性、分布性和自治性等。 ( 3 ) 由于网格资源的动态性，导致网格的计算和处理能力随时间变化，因此对网格工作 流的应用性能的估计相对困难。 ( 4 ) 在网格工作流中，计算型任务多，用户型任务相对较少，网格工作流很多是利用网 格的计算资源分布并行运行，但是由于网格的动态性，因此并行任务的执行效率相对比较低。 ( 5 ) 另外，从网格应用的实践看，网格工作流不同于传统工作流，更强调如何有效的利 用网格资源来完成相应的网格任务。 综上所述，网格工作流不仅仅是传统工作流技术和网格技术的简单结合，还有大量的问 题需要针对网格和网格应用自身的特点重新研究和考虑。因此，有必要研究面向复杂网格应 用的网格工作流处理技术。目前，基于网格环境的工作流技术还不是很成熟，对于网格工作 流的定义还不统一。 文献 9 】中将网格工作流定义为由一组网格任务组成，这些任务为实现某一特定目标，定 义良好的工作流规范，在分布的网格资源上得以执行。 。 文献0 0 1 中将网格工作流定义为多个网格服务协同合作的网格任务流程以工作流的形式 进行抽象，从而提供了一种针对具体网格应用动态整合与管理网格服务的有效方式，实现了 网格资源的整合与共享。 文献 1 1 】中将网格工作流的管理部件定义为一个公共服务，用于支持各种工作的协作。 文献 1 2 】中网格工作流则被定义为将网格服务组织成一个由这些服务的操作构成的流 程，这个流程可以看作是在某一时间段上为了完成某个特定目标的网格服务。 综合以上各种观点，将网格工作流定义为：在网格环境下，利用网格提供的资源和服务， 通过业务流程的全部或部分自动化，实现组织成员间的协调工作以达到业务的整体目标。 网格工作流具有如下优点：1 ) 协同分布的网格资源实现动态的网格应用；2 ) 实现虚拟 组织问分工协作；3 ) 使用位于特定域的资源来增加吞吐量或减少执行成本；4 ) 跨管理域执 行任务，获取网格用户所需的处理能力。 1 3 工作流的验证 工作流过程建模是一个非常复杂的过程，也是一个极易出错的过程，如果定义好的过程 在投入运行之后被发现有错，则修复错误的代价相当高。工作流验证的目的是在过程定义时 面向语义约束的协同验证研究 检验工作流的正确性，避免执行时出现异常，从而降低工作过程运行时的停产、 的成本。 1 3 1 网格工作流验证的研究现状 网格工作流是随着网格计算技术的发展而产生的一种新型协同计算技术，网格工作流的 最终目的是针对网格中用户提出的复杂问题，将网格环境下不同的网格服务按一定方式组织 起来，形成一个新的组合网格服务，用来支持建模、重构和执行大规模复杂业务流程，使得 用户能够像使用普通网格服务一样使用该组合网格服务。 为了保证网格工作流实施的正确性，对网格工作流的正确性进行验证是十分必要的。隐 含着错误的工作流模型很可能导致运行失败，在系统运行之后再更正错误耗费巨大。因此， 在工作流执行之前，需要采用验证方法，对业务过程中的各项特性进行检测，以保证工作流 模型的正确性。柔性建模方法【1 3 - 1 5 】可满足动态修改过程定义的要求，却并不保证修改后过程 定义的正确性。文献 1 6 1 分析了在工作流中使用基于p e t r i - n e t 技术的结构错误，并且提出了 一些验证算法。文献【1 7 】提出了能够解决规模问题、动态问题和选择问题的动态网格工作流 过程建模语言，动态工作流网d p e t r in e t ，并且对d p e t r in e t 的相关属性和性质，例如：可 达性，活性，正确性进行了分析，提出了相关的验证方法。文献 1 8 提出了一种叫做p g w f t 工具包，主要用于网格工作流验证及优化，该工具包结合了p e t f i 网及g u i 设计的优点，并 且作为网格工作流管理系统c g s p 19 】( c h i n a g r i ds u p p o r tp l a t f o r m ) 中的一个组件而得到应用。 文献 2 0 2 4 】讨论了实时依赖以及其对网格工作流系统有效性和效率实时验证的影响，分析了 如何在运行时间执行阶段为实时验证选择检查点，对于一个上层界限约束引入了4 个连续状 态并提出相应的验证算法。 上述是关于网格工作流验证的一些研究工作，主要解决的是网格工作流过程建模、模型 检测、检查点的选择、结构验证等问题。目前，从网格工作流语义正确性角度出发的研究相 对较少。文献 2 5 】提出了资源语义约束工作流网，并从并发控制流与其数据语义相一致的角 度出发，给出了验证算法和修改规则。文献【2 6 】提出了无数据流冲突的模式进化算法及进化 时保证控制流结构正确性的进化插入规则，并给出了相关的正确性验证。文献【2 7 】提出种 规范驱动的网格工作流系统的形式化描述方法和验证方法，使在动态模拟网格工作流系统运 行的过程中，按照给定的规则，使系统状态不断发生变化，直到系统结束。在该过程中可以 检测规则中的语义冲突，确保其完整性。文献 2 8 3 1 针对过程定义中控制流、数据流和资源 三维元信息相结合的冲突检测问题，研究了过程的语义验证方法。随着网格应用的复杂化， 4 内蒙古火学硕士学位论文 为了保证网格工作流的正确运行，通过验证技术来检测过程中的各项特性是十分必要的。 1 3 2 网格工作流验证中存在的问题 网格的动态性、分布性、异构性和自治性导致传统工作流的一些方法和技术不能处理网 格环境中的相关问题，虽然网格工作流的研究取得了一些初步成果，但在网格工作流验证中 还存在一些问题。网格工作流验证的目的是确保网格工作流描述和执行的正确性，网格工作 流描述和执行过程中不能有死锁，活锁，或资源冲突等错误发生。网格工作流验证中还有以 下问题有待于进一步的研列3 2 】【3 3 】。 ( 1 ) 语义验证 结构验证也称控制流验证，目的是验证结构的一致性。在网格工作流的描述中，主要的 结构一致性问题包括死锁、活锁、无同步等问题。目前，大部分研究主要集中在结构验证上， 然而结构验证方法只能保证控制流方面的正确性，而不足以保证过程的目标实现。例如：假 定网格工作流在结构上是正确的，活动a 后一个选择分支分别指向活动b 和c ，从工作流模 型的控制流上讲，活动a 执行后，活动b 或c 都可以被触发。然而，如果该工作流模型的语 义要求活动a 执行结束后，触发活动d ，那么工作流将不能够继续执行，该工作流模型的描 述是错误的。在工作流的过程验证研究中，语义验证【3 1 1 是层次最高的验证，且能涵盖控制流 冲突检测即结构验证，在语法验证的基础上，通过语义正确性验证，即可确定过程是否正确 实现其业务目标。 ( 2 ) 性能验证 性能验证旨在验证用户自定义的性能参数是否可以得到满足。网格工作流的执行通常与 用户定义的性能参数，如：平均活动完成时间，平均容量利用率，平均活动排队时间等参数 密切相关。进行性能验证时，首先要计算系统性能参数，然后将它们与用户预定义的参数值 进行比较。目前，人们试图利用马尔可夫链模型理论，排队理论和仿真工具进行性能参数的 计算。然而，这些方法都存在着一些问题，例如：马尔可夫链模型并不能分析网格工作流的 各个属性，并且应用马尔可夫链分析也需要消耗一定的时间【3 4 】f 3 5 】；排队理论不能分析网格工 作流过程模型3 4 】；仿真工具将网格工作流模型转化成该工具能够分析的模型，并模拟网格工 作流的执行，但是却不能同时将工作流的语义信息映射到仿真模型中。 ( 3 ) 时序验证 时序验证【3 6 1 的目的是为了检测时序约束与工作流模型的一致性，工作流系统时序约束的 表示方式一般分为绝对时i 盲 ( a b s o l u t et i m e ) 约束和相对时间( r e l a t i v et i m e ) 约束。绝对时间就是 雪塑堡墨竺壅竺堡旦鉴鲨堕壅 日历时间，绝对时间约束是限制某一时间发生的绝对时问范围。相对时间是基于某一时间参 考点的时间，相对时间约束表示两事件之间相对时间的约束。在业务流程的定义中如果包含 多个时间约束，就有可能发生冲突。相对约束和绝对约束都可能发生冲突，它们之间也有可 能发生约束冲突。如果时间约束限制的事件，其发生顺序和控制流顺序不一致，则可能造成 循环等待问题。 ( 4 ) 协同验证 协同工作是“以人为本”的，协同过程的最终目标是达成人的协作意愿。因此，只用通 过了协同验证，才能保证分布式的协同过程完成了它的目标，人们才认为这个过程完成的协 作是可信的。工作流模型的合理性验证技术一般包括三个方面：语法、结构和语义，语法的 正确性容易得到保证，语义的正确性是对工作流模型最为严格的验证，验证的范围十分广泛， 也是难点所在，而以完成协同过程的目标为目的的语义验证研究较少，还有待于补充和完善。 1 4 有关本论文 1 4 1 主要研究内容 本论文的研究工作是结合国家自然科学基金课题“面向语义约束的协同过程形式化建模 与验证的研究 进行的，主要完成了以下几方面的工作。 ( 1 ) 协同验证的概念和模型 语义验证检验工作流过程中的控制流，数据流和资源三维元信息协作的正确性，以确定 过程定义是否正确实现其业务目标为目的。协同验证是在工作流子模型不断的合成，规模逐 渐扩大的过程中，随时支持着语义验证，检验整个协同过程是否完成了协作者的目标。本文 定义了协同验证的概念，并提出协同验证具有二维性的观点。 ( 2 ) 论证协同验证过程的合理性 协同验证具有二维性，一个维度考虑规模，基于语义约束验证因地域，功能因素形成的 子模型的合成；一个维度考虑内容，基于语义约束验证协同目标的实现。本文在协同验证理 论的基础上，论证协同验证过程的合理性，整个验证过程是在协同验证的两个维度上交叉进 行的过程。这个交叉验证与“先子模型，再合成的方法在验证目的上是一致的，而在支持 动态性上具有优势。 ( 3 ) 研究协同验证的化简规则 6 内蒙古大学硕士学位论文 随着科学技术的发展，实际系统越来越庞大和复杂，网的可达状态和条件数量不断的增 加，就会由于状态空间爆炸而带来系统分析上的高复杂性。本文提出了四条基于s c n 的子网 级化简规则，使协同验证基于化简技术。在语义约束一致性的原则下，如果子网内部是无语 义冲突的，子网已经通过验证并且是正确的情况下，在验证子网合成后的模型时，把子网部 分看作一个独立的个体而忽略内部逻辑，来检查合成模型是否正确，避免不必要的重复验证， 提高了验证效率。 ( 4 ) 化简规则的有效性和完备性证明 首先将p p ，t t ，p t ，t p 四种类型的子网根据输入输出详细分类，分析了各类子网集合 中满足四条s c n 化简规则前提的所有情况，并证明了化简规则的活性保持性，最后设计了一 个网上购物实例证明了化简规则的有效性。 1 4 2 主要贡献和创新点 本文围绕网格环境下、面向协同应用的，大规模复杂流程的协同验证问题展开研究，重 点解决协同验证理论的提出，论证交叉验证的合理性与协同验证的化简规则设计三大问题， 其主要贡献和创新点如下。 ( 1 ) 提出协同验证的概念和模型 目前的验证多数基于控制流结构进行，而以完成协同过程的目标为目的的语义验证较少。 协同验证首先体现在协作目标的验证上。其次，网格中存在跨组织，跨域的协作，形式化的 即可抽象为子模型的协作，因此协同验证还包含基于语义约束的合成验证。 ( 2 ) 论证交叉验证过程的合理性 根据子模型之间关系的不同，定义了7 种s c n 的协作方式：顺序协作、与分支协作、或 分支协作、异或分支协作、与合并协作、或合并协作、异或合并协作。论证了交叉验证与“先 子模型，再合成 的方法在验证目的上是一致的，而在支持动态性上具有优势。 ( 3 ) 提出协同验证的化简规则 基于s c n 提出一组子网级化简规则，这组规则将已经通过验证并且是正确的子网看做一 个整体，根据子网入口与出口的不同，提出p p 型，t t 型，p t 型，t p 型四条子网级化简规 则，并证明了这组子网级化简规则的活性保持性。 1 4 3 论文结构安排 本论文各章节组织如下： 7 第一章弟一早 存在的问题 第二章 作方式，提 用提供了基 第三章弟二早 p t 型和t p 提出四条化 第四章峁凹早 并应用第三 第五章弟丑早 8 内蒙古大学硕士学位论文 第二章网格工作流的协同验证理论 2 1c s c n 的基本概念 2 1 1p e t r i 网的基本概念 p e t r i 网是一种系统建模与分析工具，以并发论，网逻辑和网拓扑为主要内容，它同时具 有充分的模拟能力和丰富的分析方法。下面给出p e t r i 网【3 7 。4 川的定义。 定义1 ( p e t f i 网) ：p e t r i 网是一个四元组p n = ( p , t , f , m o ) ，其中： ( 1 ) p = p l ，p 2 ，p m 是库所的有限集合； ( 2 ) t = t l ，t 2 ，t n ) 是变迁的有限集合； ( 3 ) p u t ，p n t = o ； ( 4 ) f ( ( p t ) u ( t x p ) ) 表示库所和变迁之间的流关系； ( 5 ) d o m ( f ) uc o d ( f ) = put ( 不存在孤立元素) ； d o m ( f ) = x i 了y ：( x ，y ) f ； c o d ( f ) 2 x l 了y ：( y ；x ) f ) ； ( 6 ) 映射m o ：p 一 0 , 1 ，2 ，) 是网的初始标识。 有向图n = ( p ，t ；f ) 是p e t r i 网的基网，不包含初始标识，一个p e t r i 网也可以表示y o ( n ，m o ) 。 定义2 ( 前置集和后置集) ：设网p n = ( p , t , f , m o ) ，对x p ut ，记 + x 。 yj y p u t a x ) f ) x 一 y l y e p u t 人( x ，y ) e f 称x 为元素x 的前置集，x 为x 的后置集，x u x 为x 的外延。 定义3 ( 变迁的使能与点火) ：设p n = ( p , t ；f , m o ) 是一个p e t r i 网，称变迁t t 在标识m o 下 是使能的，当且仅当对v p t ，都有m o ( p ) 1 ，记作m o t 。在m o 下使能的变迁t 可以引发， 引发后得到的后继标识为m ，则 i ( p ) 一1劾，一， m ( p ) = m o ( p ) + 1e p f f i m o ( p ) 否则 9 记作m 0 m 。 变迁t 为死的( d e a d ) ；若对vm er ( m o ) ，都有m r ( m ) ，使得m p ，则称变迁t 为活i 拘( 1 i v e ) 。 如果对v t t 都是活的，则称该p h i 为活的p e t r i 网。 一个活的p e t r i 网无论选择怎样的变迁引发序列，都可以保证无死锁操作。 2 1 2 语义约束网s c n 语义约束网( s e m a n t i c sc o n s t r a i n t sn e t ，s c n ) 是在三维工作流网【2 8 1 的基础上，增加了网格资 源动态性的描述，并把网格工作流中业务执行的各种数据、组织者和资源都转化为p e t r i 网的 颜色集。本节给出文献【4 1 】中s c n 的形式化定义如下。 定义6 ( 语义约束网s c n ) ：设，kr ，r 分别表示工作流过程中的活动名、数据对象名、 组织对象名和资源的集合，则一个语义约束网是一个八元组s c n = ： p 是库所的有限集合；t 是变迁的有限集合； pn t = ；put ，ji , o ep ，i = o ，o = ，p = p 。up r ，t = t ut iu t i nu t o i i ，其中p a 是普通 库所的集合，p ，是资源库所，t 为内部变迁，t i 活动变迁，t i n 输入变迁，输出变迁； f c ( p x t ) u ( t p ) 是弧集合，且f r uf o o f , f ，为所有连接资源库所的弧，f o 为禁止弧； c 是托肯类型的有限非空集合，且c = c d u c ，u c 。u ) ，其中c d 表示数据类型，c ，表示 资源的属性关联关系，c 。表示组织类型，为缺省值； g 是防卫函数，定义在t 上的表达式，且t t t y p e ( g ( t ) ) = b ，b = t r u e ，f a l s e ； l a b ：t _ ，c d k ，c e r ，c ，一s 为标记函数； e x p ：f - - - ，n x c x c o n 是弧表达函数，其中，n = 1 ，2 ，) ，c o n 是可以完成计算、比较和逻辑操 作的条件表达式，c o nc o n 的结果取值为布尔类型，即：t y p e ( c o n ) = b ； m o ：p a 一 ，似c d u c 。u ) ) ) ，p r 一 ，c ，) 是初始网标识，p c 是c 的多集 s c n 在3 d w f n 的基础上增加了资源动态性，使其不仅满足了网格工作流是动态工作流 的特点，而且能体现网格工作流中数据、执行者、资源等信息，实现了网格工作流的全面性 描述。 1 0 塑蓥点叁堂堡堂堡笙茎 定义7 ( s c n 的活性) ：设= 是一个s c n 网系统： ( 1 ) 变迁t t 是活的，当且仅当v me r ( m o ) ，v m r ( m ) ，使得m 【t ： ( 2 ) 是活的，当且仅当v t t ，t 是活的； ( 3 ) s c n 是活的，当且仅当存在标识m o ，使得( n ，m o ) 是活的。 p e t r i 网的动态行为表现为托肯的迁移，在基本p e t r i 网描述的工作流过程中，托肯的迁移 只表示控制权( 或称执行权) 在活动之间的交接，从而体现业务过程的执行。下面，通过解释 s c n 的动态语义，说明数据沿控制流进行传递和任务执行所需要资源的申请和释放。 2 1 3s c n 的协作方式 运用p e t r i 网作为工具来给工作流建模，国内外很多专家都已经有不少工作，其中最为著 名的就是a a l s t ，文献 4 2 4 3 1 通过改进传统p e t r i 网的变迁，提出了2 0 种工作流模式。本文参 考工作流的基本模式，针对子网之间的关系不同，定义了7 种s c n 协作方式。下文以u 表 示s c n 子网，并且忽略了子网内部的具体流程。_ 表示子网发生的先后次序。 根据子网接口元素的不同，将子网分为四种基本类型，分别为p p 型、n 型、p t 型、t p 型【4 1 1 。n o = 是s c n 的一个子网，y f 且 p i ，p 。) _ cp o ， t i ，t o - - - t o ： 若满足t ( 1 ) 若p i 是n o 唯一的输入库所，p o 是唯一的输出库所，则称n o 为p p 型子网。 ( 2 ) 若t i 是n o 唯一的输入变迁，t 0 是唯一的输出变迁，则称n o 为t t 型子网。 ( 3 ) 若p i 是n o 唯一的输入库所，t 0 是唯一的输出变迁，则称n o 为p t 型子网。 ( 4 ) 若t i 是n o 唯一的输入变迁，p o 是唯一的输出库所，则称n o 为t p 型子网。 这里只是对子网类型的简单描述，关于子网的详细形式化定义参考3 1 节，下面给出s c n 子网的协作方式。 1 顺序协作方式 当两个或更多的子网之间存在依赖性时，前一子网内活动完成前，后一子网内活动不能 被启动，这时需采用子网顺序协作方式。子网顺序协作方式的示意图如图2 1 所示，图中a 与b 分别表示两个子网，它们以顺序的方式连接在一起，子网b 的执行要在子网a 中的活动 全部执行结束后才能开始。例如：在网上购物流程中，首先客户要填写订单，只有实现“下 订单”功能的子网流程完成后，才能激活“客户付款 的子网流程。 子网顺序协作方式共有1 6 钟情况：( 1 ) a ，b 都为p p 型子网；( 2 ) a 为p t 型子网，b 为 p p 型子网；( 3 ) a 为t p 型子网，b 为p p 型子网；( 4 ) a 为t t 型子网，b 为p p 型子网；( 5 ) a 图2 2 与分支协作方式的子网合成示意图 f i g u r e 2 2t h es y n t h e s i so f t h ea n d - s p l i tc o o p e r a t i o no f t h es u b n e t 3 与合并协作方式 1 2 内蒙古人学硕十学位论文 当两个或多个子网汇聚成一个控制线程时，需采用与合并协作方式。子网与合并协作方 式示意图如图2 4 所示，a n d - j o i n 表示“与合并 关系。子网a 、b 、c 为与合并协作关系， 子网a 的执行要在子网b 、c 中的活动全部执行结束后才能开始执行。例如：在模拟快餐店 流程中，“顾客选餐 与“顾客付款 流程结束后，激活“上菜 流程。 注：为了方便，本节中所举的例子，仅用单一活动的名称代表了整个子网所完成的功能。 例：在完成“顾客选餐功能的子网中，包括顾客查看菜单，选菜，服务员记录菜谱，计算 顾客应付金额等活动，而非单一的顾客选餐活动。 4 或分支协作方式 当要从一个给定的可选子网分支集中选择多条分支执行时，需采用或分支协作方式。子 网或分支协作方式示意图如图2 5 所示，o r s p l i t 表示“或分支”关系。子网a 、b 、c 为或 分支协作关系，当子网a 中的活动全部执行结束后，子网b 或c 可以开始执行。例如：在商 店购物流程中，有两种付款方式：“交现金或“使用购物券 ，顾客可以任选其一。另外， 如果客户想购买5 0 0 元的商品，但只有3 0 0 元的购物券时，可以同时使用两种付款方式。 5 或合并协作方式 当某个合并可能有多于一个输入被激活，那么必须等到所有可能的输入都