（计算机软件与理论专业论文）基于π演算的wsbpel建模与实现.pdf

摘要 业务流程的设计和验证是所有工作流产品的一个主要功能。为了能够尽早发现流程 建模中死锁、缺少同步等问题，大部分工作流产品都需要提供基于形式化分析和建模的 功能。由于w s b p e l ( w 曲s e r v i c e sb u s i n e s sp r o c e s se x e c u t i o nl a n g u a g e ) 描述业务流程 是半形式化的，不易检测与验证，也没有相应形式化工具支持，这使得w | e b 服务组合的 正确性难以保证，其业务流程也无法在较抽象的层次上进行跟踪。 本文结合实验室承担的国家8 6 3 科研攻关项目，针对业务流程内部逻辑的正确性问 题展开研究，探索利用进程代数一演算作为形式化工具，对w s b p e l 描述的业务流程 进行建模和验证。主要进行的工作如下： 1 本文提出了业务流程建模与验证的体系结构b p m v ( b u s i n e s sp r o c e s sm o d e l i n ga n d v e r f i c a t i o n ) 、说明了本文要解决问题及所采取的步骤，分析了基于p e t r i 网、自动机 理论、进程代数对w s b p e l 活动进行建模的方法和成果。 2 本文分析了国内外基于一演算对w s b p e l 活动建模的相关研究现状。说明了一 演算适合对w s b p e l 活动进行建模的原因，完善了一演算对w s b p e l 活动的建 模，在此基础上给出了w s b p e l 至u 一演算整体转换的算法描述。 3 针对业务流程中可能存在的死锁、活锁、互模拟问题，本文结合实例用一演算对 业务流程性质进行了分析、推演，并用m w b ( m o b i l i t yw o r k b e n c h ) 进行了验证。 4 基于e c l i p s e 开发环境和s w t 插件，设计和实现了b 2 p 原型工具。 关键字：业务流程，b p m v ，w s b p e l ，一演算，m w b a bs t r a c t b u s i n e s sp r o c e s sd e s i g na n dv e r i f i c a t i o ni sam a j o rf e a t u r eo fa l lw o r k f l o wp r o d u c t s i n o r d e rt od e t e c td e a d l o c k ，l a c ko fs y n c h r o n i z a t i o na n do t h e ri s s u e s ，m o s tw o r k f l o wp r o d u c t s n e e dt op r o v i d ea n a l y s i sa n dm o d e l i n gf u n c t i o n sb a s e do nf o r m a l i z a t i o n w s b p e l ( w e b s e r v i c e sb u s i n e s sp r o c e s se x e c u t i o nl a n g u a g e ) d e s c r i b e sb u s i n e s sp r o c e s ss e m i f o r m a l l y , w h i c hi sh a r dt od e t e c ta n dv e r i f ya n di sa l s ow i t h o u ts u p p o r to f c o r r e s p o n d i n gf o r m a lt o o l s i t c a u s e sd i f f i c u l t yi ne n s u r i n gt h ea c c u r a c yo fw e bs e r v i c ec o m p o s i t i o na n dt r a c k i n gt h e b u s i n e s sp r o c e s sa ta na b s t r a c tl e v e l t h et h e s i s ，c o m b i n e dw i t ha n8 6 3p r o j e c tu n d e r t a k e nb yt h el a b ，r e s e a r c h e so nt h e c o r r e c t n e s so fb u s i n e s sp r o c e s si n t e r n a ll o g i ca n d e x p l o r e saw a y t om o d e la n dv e r i f yb u s i n e s s p r o c e s sd e s c r i b e di nw s b p e lu s i n gp r o c e s sa l g e b r ap i - c a l c u l u sa saf o r m a lt 0 0 1 1 t h et h e s i sp u t sf o r w a r dt h ea r c h i t e c t u r eo fb p m v ( b u s i n e s sp r o c e s sm o d e l i n ga n d v e r i f i c a t i o n ) a r c h i t e c t u r e ，t h ep r o b l e mt ob es o l v e da n dt h es t e p st ob ef o l l o w e d ，a l s o a n a l y s e st h em o d e l i n gm e t h o db a s e do np e t r in e t ，a u t o m a t at h e o r y , p r o c e s sa l g e b r a 2 t h et h e s i sa n a l y z e sr e l a t e dr e s e a r c hu s i n gp i c a l c u l u sm o d e l i n gw s b p e la th o m ea n d a b r o a d ，s u m su pt h er e a s o no ft h ep i - c a l c u l u ss u i t a b l ef o rm o d e l i n gt h ew s - b p e l ，t h e n t h ep a p e rm o d e l st h ea c t i v i t i e so fw s b p e l o nt h eb a s i s ，w ep r e s e n ta l g o r i t h m d e s c r i p t i o nf o rp i c a l c u l u s b a s e dm o d e l i n go fw s - b p e l 3 t h et h e s i sa n a l y z e st h ep r o p e r t y , s u c ha sd e a d l o c k ，a l i v e l o c k ，b i s i m u l a t i o n ，w h i c hm a y e x i s ti nb u s i n e s sp r o c e s s ，d e d u c e st h ep r o p e r t yb yp i c a l c u l u sa n dv e r i f i e st h ep r o p e r t yb y m w b 4 b a s e do ne c l i p s ed e v e l o p m e n te n v i r o n m e n ta n ds w t p l u g i n d e s i g na n di m p l e m e n tt h e p r o t o t y p et o o lo fb 2 e k e y w o r d s ：b u s i n e s sp r o c e s s ，b p m v , w s b p e l ，p i - c a l c u l u s ，m w b 西北大学学位论文知识产权声明书 本人完全了解西北大学关于收集、保存、使用学位论文的规定。 学校有权保留并向国家有关部门或机构送交论文的复印件和电子版。 本人允许论文被查阅和借阅。本人授权西北大学可以将本学位论文的 全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫 描等复制手段保存和汇编本学位论文。同时授权中国科学技术信息研 究所等机构将本学位论文收录到中国学位论文全文数据库或其它 相关数据库。 保密论文待解密后适用本声明。 学位论文作者签名：孟醴龟：指导教师签名：跹 2 。p 年月，7 曰枷7 年z 月1 7 日 西北大学学位论文独创性声明 本人声明：所呈交的学位论文是本人在导师指导下进行的研 究工作及取得的研究成果。据我所知，除了文中特别加以标注 和致谢的地方外，本论文不包含其他人已经发表或撰写过的研 究成果，也不包含为获得西北大学或其它教育机构的学位或证 书而使用过的材料。与我一同工作的同志对本研究所做的任何 贡献均已在论文中作了明确的说明并表示谢意。 学位论文作者签名：于稍伟 2 0 田年f 月f 7 日i - - - i v v ，u ，j ， 两北人学硕l 学位论文 1 1 研究背景 第一章绪论 近年来，i n t e m e t 网络已经变成一个巨大的商业平台，使得越来越多的组织和个人相 互通信更加方便，快捷。它使得基于网路的商业活动或者服务不断增值。由于w e b 服务 的出现，为不同组织或个人的特定应用的互操作提供了可行性，所以w e b 服务受到越来 越多的关注。 w e b 服务是部署在i n t e m e t 上使用诸如x m l ( e x t e n s i b l em a r k u pl a n g u a g e ) 、s o a p ( s i m p l eo b j e c ta c c e s sp r o t o c 0 1 ) 、w s d l ( w e bs e r v i c e sd e s c r i p t i o nl a n g u a g e ) 和u d d i ( u n i v e r s a ld e s c r i p t i o nd i s c o v e r ya n di n t e g r a t i o n ) 等w e b 标准的技术，其主要目的就是 在现有的各种异构平台基础上构筑一个通用的与平台无关、语言无关的技术层，使得不 同平台之上的应用依靠这个技术层来实施彼此的连接和集成，提供种开放的发展平 台，用于使用、展开、连接和管理分布于全球网络服务。w e b 服务所使用的x m l 可以用 真正与平台无关的方式来描述任何数据，以跨系统交换数据，因此转向了松耦合应用程 序。w e b 服务还可以在较抽象的层面上工作，较抽象层面可以按照需要动态地重新评估、 修改或处理数据类型。所以从技术层面上讲，w e b 服务可以更方便地处理数据，并且允 许软件更自由地进行通信。从更高的概念层面上讲，可以将w e b 服务视为一些工作单元， 每个单元处理特定的功能任务。单个的服务很难满足客户的需求，客户需要的服务通常 是由一系列不同的w e b 服务提供者提供的服务交互协作完成。为了能充分利用共享的 w e b 服务满足复杂的业务需求，这使得w e b 服务组合研究的成为了新的发展方向。 所谓w e b 服务组合由各个小粒度的w e b 服务相互之间通信和协作来实现大粒度的服 务功能；通过有效的联合各种不同功能的w e b 服务，服务开发者可以借此解决较为复杂 的问题，实现增值功能。w e b 服务的真正价值在于服务之间的交互，而不在于w e b 服务 自身的个别优点。当业务流程能够通过使用标准流程集成模型，集成复杂的交互时才能 发挥w e b 服务作为集成平台的全部潜力i l l 2 1 。基于x m l 的业务流程执行语言 b p e l ( b u s i n e s sp r o c e s se x e c u t i o nl a n g u a g ef o rw e bs e r v i c e s ，简称b p e l ) ，提供了这样 的一个标准集成模型。 b p e l 结合了i b mw s f l 和m i c r o s o f tx l a n g 两门语言的优点，同时摈弃了一些复杂 繁琐的部分，形成一门较为自然的描述商业活动的抽象语言，它为描述w e b 服务组合流 第一章绪论 程的控制流、数据流指定了语法规则。2 0 0 3 年3 月发布了b p e l 4 w s l 1 版本。同年4 月， b p e l 被提交结构化信息标准促进组织( o a s i s ) 以实现标准化，2 0 0 7 年5 月o s a s i s 推出了 w s b p e l2 0 。目f ； 已经成为服务组合语言的事实标准，它为基于w e b 服务的业务流程 行为交互定义了一种表示方法，也提供了将已经存在但单- - w e b j l 曼务组合成复杂的服务 组合，经过人工设计或自动构建完成的服务组合可能存在众多问题。虽然很多b p e l 设 计工具可以帮助发现w s b p e l 中的语法错误，但是流程潜在的逻辑错误不能被完全消 除。 由于业务流程执行语言w s b p e l 描述业务流程是半形式化的，不易检测验证，也没 有相应形式化工具支持，这使得w e b 服务组合的f 确性难以保证，其业务流程也无法在 较抽象的层次上跟踪。为了有效的发现和解决基于w e b 服务的业务流程中组合之间的死 锁、活锁、服务兼容性等问题，确保基于w e b 服务的业务流程的正确运行。需要有一种 好的发现错误的方法。 形式化方法是在2 0 世纪6 0 年代末为了解决“软件危机”而发展起来的。所谓形式化 方法是一种基于数学的描述系统特性的技术，包括各种语言、技术和工具等【3 】。它分为 形式规范方法和形式验证方法两大类。形式化方法提供了以系统的方式，而不是以约定 俗成的方式，描述、开发和验证系统的框架结构，数学基础和形式化规范语言是形式化 方法的基本组成元素。形式化方法的意义在于它能帮助发现其它方法不容易发现的系统 描述的不一致，不明确或不完整，有助于增加软件开发人员对系统的理解1 4 1 。我国有不 少高校和研究所从事形式化方法及相关理论方面的研究工作，包括南京大学、国防科技 大学、上海交通大学、同济大学、东南大学、北京航空航天大学、中科院软件研究所等， 其中有代表性的中科院软件研究所林惠民院士有关并发进程代数理论及验证工具、上海 交通大学傅育熙教授b a s i c s 实验室有关并发理论的研究、同济大学蒋俊昌教授等人有 关在p e t r i 网基础理论、建模、分析验证的研究。 在省市科委和图家8 6 3 计划的支持下，西北大学软件工程研究所一直致力于工作流、 服务组合相关技术的研究，其中有代表性是与西安协同软件公司共同开发的基于w e b 的 工作流管理系统s y n c h r o f l o w ，并已经成功投入市场，取得多项成果【5 】【6 】【7 j 【8 】【9 】【1 0 1 【l l 】。 本文工作是国家8 6 3 计划信息技术领域高可信软件生产工具及集成环境专题面向 流程管理的软件生产线课题研究( 2 0 0 7 a a 0 1 0 3 0 5 ) 的一部分。本项目旨在研究和解决跨组 织分布式流程模型、流程管理软件生产线可信性分析与评估方法、流程模型检查与验证 技术、基于m d a ( m o d e ld r i v e na r c h i t e c t u r e ) 的可视化工具集成环境设计与实现。项目 2 两北大学硕l ：学位论文 由西北大学、西安协同软件产业( 集团) 股份有限公司、清华大学、西安理工大学四家共 同承担研制。在该项目中，西北大学主要负责理论研究、核心技平台研发。而本文工作 则是子课题基于一演算业务流程形式化建模与分析部分研究内容。 业务流程的设计和验证是所有工作流产品的一个主要功能。为了能够尽早发现流程 建模中死锁、缺少同步等问题，许多工作流产品都需要提供基于形式化分析和建模的功 能。8 6 3 项目成员西安协同软件公司的工作流平台s y n c h r o f l o w 流程模型是基于令牌驱动 的p e t r i 网流程模型很好解决了流程元素固定的流程表达能力问题，而对于流程元素不 固定的、动态的流程，利用p e t r i 网则很难描述动态变化的模型。 一演算是一种移动进程代数，它支持传递通道名的特征使得它能描述结构动态变 化的系统，可使用它来描述服务组合的动态变化。本文利用一演算建模w s b p e l 活动 和基于w s b p e l 的业务流程，对业务流程的性质进行分析，为建立动态变化的业务流程 模型进行有益的探索。 1 2 国内外研究现状 w e b 服务组合验证是w e b 服务组合的一个关键步骤，它能提前发现w e b 服务组合中 存在的问题，以确保正确可用的服务组合投入使用，从而提高服务组合执行的成功率和 用户满意度，它是企业构建正确的基于s o a 的应用系统的重要保障。因此，探索和研究 w e b 服务组合验证具有重要意义【1 2 1 。w s b p e l 作为w e b 服务组合的描述语言，用形式化 的方式对w s b p e l 进行建模与验证，同样也是非常重要的。 纵观目前国内外有关对用w s b p e l 描述的w e b 服务组合进行验证都是基于某种形 式化的方法进行，主要有p e t r i 网、自动机理论和进程代数三种方法。 p e t r i 网不仅具有直观的图形表示方法和丰富的形式化语义，而且提供了很多系统的 分析验证手段，因此p e t r i 网被作为一种形式化工具而被广泛应用于流程分析与验证。文 献 1 3 采用p e t r i 网对b p e i a w s 进行建模，用w o m b a t 4 w s 进行验证b p e l 描述流程的一致 性。文献 1 4 提出一种基于c p n e t s 的分析方法对b p e l 4 w s 描述的业务流程进行从 b p e l 4 w s 到c p n e t s 的映射，基于这些规则可以将b p e l 流程转换成c p n 模型，然后使用 c p n 工具进行分析和验证。文献 1 5 采用分层p e t r i 网对w s b p e l 的流程进行建模，并用 工具h p s i m 对w s b p e l 流程进行分析与验证。 基于自动机理论对b p e l 形式化建模研究：文献 1 6 用卫式自动机( g u a r d e d a u t o m a t o n ) 来描述服务，文中给出了b p e l 4 w s 部分活动到卫式自动机的转换方法，它们 第一章绪论 是 、 、 、 、 五种活动。文献 1 7 1 8 给出一 套技术和工具( g u a r d e da u t o m a t a 、p r o m e l a 语言，s p i n 模型检测工具) 和完成的系统分析 和验证w e b 服务的方法，可方便地使用工具分析组合w e b 服务的正确性。文献 1 9 采用 有限状态机对基于b p e l 描述的服务组合流程进行建模，通过检验流程的安全性和活性 等属性来验证组合服务的正确性。文献 2 0 中，将组合描述语言w s f l 转换成p r o m e l a 规 范语言来描述，s p i n 提供了模型检查功能。类似的对于b p e l 就需要制定相应的转换规 则。 进程代数是一类使用代数方法研究通信并发系统的理论的泛称，它包括了通信系统 演算( c a l c u l u so f c o m m u n i c a t i n gs y s t e m s ，c c s ) 、通信顺序进程( c o m m u n i c a t i o ns e q u e n t i a l p r o c e s s ，c s p ) 和一演算等。 m k o s h i n a 和f v a n b r e u g e l l 2 1 】提出了利用c c s 对b p e l 4 w s 建模，用c w b m n c 来检验w e b h 艮务组合。文献 2 2 研究了进程代数与b p e l 4 w s 的双向映射问题。用进程 代数提供的工具对b p e l 4 w s 文件进行设计和性质的检验。文章 2 3 同样利用c c s 对 b p e l 4 w s 建模，并用进程表达式的形式化模型来分析w e b 服务行为的可替换性和兼容 性。文献 2 4 中提出将b p e l 程序转换成f s p 进程并且使用t l s a t 具来验证f s p 进程。 t l s a 工具允许用户以确定性f s p ( f i n i t es t a t ep r o c e s s ) 进程来指定属性，在文献中描述了 t l s a 工具的w s b p e l 插件。这种建模方法也是将服务流程描述转换成相应的f s p 模型 的描述方式，然后再进行分析验证。 国内外也有一部分学者用丌一演算来建模w s b p e l 活动，论文的第四章进行详细介 绍。 1 3 研究内容 本文主要围绕8 6 3 项目子课题基于一演算业务流程形式化建模与分析要解决的 问题展开研究，主要研究内容包括如图1 1 所示： 4 西北火学硕l 二学位论文 图1 1 研究内容示意图 1 介绍了业务流程建模与验证b p m v 的框架、描述了本文要解决的问题及所采取的技 术路线：对基于p e t r i 网理论、自动机理论、进程代数理论建模w s b p e l 活动的典 型方法进行介绍，并且分析了基于三种形式化方法建模的原理和已有的研究成果。 2 对兀一演算和w s b p e l 基础内容进行介绍，为基于一演算的业务流程的自动建模 与验证工具b 2 p 的实现提供理论基础和技术背景。 3 分析和总结了国内外一演算建模w s b p e l 活动的相关研究现状。给出了一演算 适合建模w s b p e l 活动的原因和w s b p e l 与一演算的概念对应；用一演算对 w s 。b p e l 中的原子活动、结构化活动、流程处理器( 补偿活动、事务处理、故障处 理) 进行了描述；给出了用w s b p e l 描述的业务流程文件到一演算描述的算法描 述。 4 结合课题组研究的内容，本文着重对业务流程的死锁、活锁、互模拟性质进行了分 析、并用一演算和m w b 工具进行了推演和验证。 5 在验证工具m w b 基础上，设计和实现了b 2 p 原型工具。 1 4 论文的组织结构 全文共分为六章，其中： 第一章绪论 介绍了w e b 服务及其组合形式化分析与验证的必要性和重要性，以及本文选题的 来源；总结了国内外已有的对业务流程描述语言w s b p e l 建模与验证的研究现状；最 后，详细介绍本文所做的工作。 第二章相关研究 本章给出了业务流程验证的框架体系结构图和对用w s b p e l 描述业务流程进行性 质分析与验证所应遵循的步骤，最后介绍了已有w s b p e l 活动建模与验证的典型方法 ( 基于p e t r i 网理论、自动机理论、进程代数理论) 。 第三章一演算与b p e l 本章对一演算的基础理论介绍包括一演算的语法、约简规则、操作语义、等价 理论及针对一演算开发的验证工具移动工作台。对业务流程描述语言w s b p e l 介绍 包括b p e l 的发展历程、所做的变更及扩展、b p e l 的特性、b p e l 模型、b p e l 活动。 第四章w s b p e l 活动的建模与流程的性质分析 5 第一章绪论 本章主要介绍一演算建模w s b p e l 活动已有的国内外相关研究现状；分析了一 演算建模w s b p e l 活动的原因；利用一演算对w s b p e l 活动进行建模；介绍了 w s b p e l 描述的业务流程向一演算转换算法。对业务流程性质进行分析( 流程中死锁、 活锁、互模拟) ，并结合实例用一演算进行推演和移动工作台m w b 进行了验证。 第五章w s b p e l 转换和验证工具b 2 p 的设计与实现 本章主要介绍了b 2 p 工具的体系结构、功能描述及设计与实现。最后用实例进行说 明。 第六章总结与展望 本章总结了论文所做的工作及本文需要进一步完善改进的地方。 6 西北大学硕，l ：学位论文 第二章相关研究 本章首先对论文要解决的问题进行描述，提出了业务流程建模与验证的b p m v 框 架并提出达到目标所需执行的路线图。讨论了当前主要的三种形式化理论建模 w s b p e l 活动的过程。同时简要分析了基于p e t r i 网理论、自动机理论、进程代数理论 建模w s b p e l 活动的研究成果。 2 1 问题描述 业务流程是一组逻辑上相关的业务活动，这些活动联合起来向客户传递某些有价值 的东西( 如产品、货物、服务或信息) 。对业务流程描述、建模与验证的研究主要解决的 问题是在业务流程实施之前对其进行正确性和合理性的分析，确保业务流程高效、有序 地运行。为了清晰描述业务流程的建模和验证过程，本文提出了业务流程建模与验证的 体系结构b p m v ( 如图2 1 所示) 。业务流程描述层：用w s b p e l 或者b p m l 等语言来 描述业务流程。形式化模型层：用形式化工具建模业务过程。验证层：对业务流程的性 质进行分析与验证。本文要解决的问题：用形式化工具来描述和验证w s b p e l 描述的 业务流程。 图2 1 业务流程建模与验证的体系结构 解决步骤： s t e p l ：w s b p e l 活动建模( m o d e l i n g ) ：该部分为w s b p e l 文件建立形式化模型， 使用验证工具能够接受的形式语言来描述文件。在形式化过程中应该对系 7 第_ 二章相关研究 统进行一定程度的抽象，去除不必要的信息。 s t e p 2 - w s b p e l 性质描述( s p e c i f i c a t i o n ) ：该部分阐明所要验证的性质，由于业 务流程逻辑的复杂性，需要用形式化的语言来描述w s b p e l 。 s t e p 3 ：w s b p e l 验证( v e r i f i c a t i o n ) ：根据选用的形式化模型使用相应的验证工具检验 业务流程。 本文将选用进程代数之一一演算作为建模w s b p e l 活动的形式化工具，依照上 面所述的三个步骤来完成论文。 2 2 建模w s b p e l 活动的典型方法- p e t r i 网理论 p e t r i 网是德国数学家c a r la d a mp e t r i 定义的一种通用的模型，用以描述存在条件 与事件间的关系，是一种网状信息流模型，它包括两种类型的节点：库所( p l a c e ) 和变迁 ( t r a n s i t i o n ) ，而标记( t o k e n ) 存在于库所之中，表示相应的状态信息，并按引发规则驱动 事件发生，从而反映整个系统的动态行为过程。p e t r i 网是一种系统建模与分析工具，以 并发论、网逻辑和网拓扑为主要内容，它同时具有充分的模拟能力和丰富的分析方法。 现在p e t r i 网己经发展成为一个庞大的研究领域。 1 p e t r i 网定义汹3 一个p e t r i 网是一个三元组- zd ，式中：p 和丁分别是库所和变迁的有限结合， 满足尸n ，= o ，尸u 丁f 2 j ，p 其中囝表示空集。f 是有一个尸元素和一个r 元素组成 的有序偶的集合，叫做流关系，满足f ( p x t ) u ( p x 丁) ，是两集合的笛卡尔乘积； 令f 所含有序偶的第一个元素和第二个元素所成的集合分别为d o m ( f ) 和c o d ( f ，满足 d o m ( du c o d ( d = p u 丁。这意味着不能有孤立元素尸、丁，且尸、丁、f 均不能为空 集。把不属于d o m ( d 和c o d ( d 的元素叫做孤立元素。 基本p e t r i 网模型的结构元素包括：用圆表示的库所( p l a c e ) ，用长方形表示的变迁 ( t r a n s i t i o n ) 及带箭头的弧( a r c ) 。系统的状态通过库所中包括多少个托肯( t o k e n s ) 来描述。 托肯用包含在库所中的实心圆点表示。它反映库所代表的局部状态的动态实现情况。 2 p e t r i 网建模与验证的原理 用p e t r i 网对业务流程进行建模，主要目的之一就是借助p e t r i 模型来分析w s - b p e l 描述实际问题的性质与功能。由于p e r i 网有丰富的图形表现形式，用网能直观构造业务 流程的模型，描述它的物理结构。如果用p e t r i 网模型确切的描述了问题的业务逻辑， 8 两北人学硕上学位论文 那么业务逻辑中存在的问题也能由p e t r i 网模型的基本理论( 可达性、不变量分析、简约 规则) 和相应的验证工具发现。 3 普通p e t r i 网与w s b p e l 模型中的一些活动的映射 和 活动被映射为p e t r i 网的变迁( t r a n s i t i o n ) ，如图2 2 所示。一个 活动被表示为一个入库所的变迁，而 活动被表示为一个出库所的变迁。 用库所表示活动执行的前提条件和后续状态。 a c t i v i t y o u t 图2 2p e t r i 网的变迁 顺序活动 s e q u e n c e ) 表示多个任务按照顺序进行。用p e t r i 网建模顺序活动如图2 3 所示。 a b t ( a ) t ( b ) 图2 3 顺序活动的p e t r i 网模型 并发活动 表示多个任务并行或者以任意次序执行，并行的任务执行完毕后执 行下一个任务。如图2 4 所示，a 、b 、c 和d 组成的并行活动模型映射为p e t r i 网模型。 其中t ( b ) 、t ( c ) 表示并行变迁。 a bc d 9 第- 二章相关研究 图2 4 并发活动的p e t r i 网模型 循环活动 ，表示某个任务多次重复执行，p e t r i 网模型如图2 5 所示。 b 口一i 图2 5 循环活动的p e t n 网模型 选择活动 ，表示前一步活动执行完后，下一步从多个任务中选择一个执行， 如图2 6 所示。 a b c d t ( b ) 图2 6 选择活动的p e t r i 网模型 4 p e t r i 网建模w s b p e l 活动已有的研究成果 在实际应用过程中，人们提出了p e t r i 网的很多子类，如着色p e t r i 网、时延p e t r i 网、分层p e t r i 网、谓w i 五- 变迁网、时间p e t r i 网、模糊p e t r i 网及受控p e t r i 网等，这些内 容的提出得以定性、定量的分析系统模型，缩减系统描述规模，有效地增强了p e t r i 网 1 0 西北大学硕i ? 学位论文 的描述能力，拓展了p e l r i 网的应用范围。 文献 2 7 将b p e l 流程分为逻辑层、语义层。其中逻辑层控制流表达了流程活动间 的依赖关系。然后将定义在逻辑层的活动映射到同步p e t r i ，进而分析流程中畅通性和无 冗余变迁性等性质。 文献 2 8 采用p e t r i 网对b p e l 建模，验证了b p e l 的全局抽象流程与每一参与者的 可执行子流程之间的一致性，检验子流程是否可以正常交互。 着色p e t r i 网( c p n e t s ) 是对普通p e t a l 网的扩展，在着色p e t r i 网中库所和变量都是有类 型说明的，使之可以支持不同类型的标记，能区分出网中流动的托肯，为表达数据流提 供了可能，也有效的减少了网络规模。弥补了p e t r i 网无数据和层次概念的不足。文献 1 4 提出一种基于c p n e t s 的分析方法对w s b p e l 流程进行从w s b p e l 至j j c p n e t s 的映射规 则，基于这些规则可以将b p e l 流程转换成c p n 模型，然后使用c p n 工具进行分析和验 证。 层次p e t r i 网的提出，可以将复杂系统进行有层次地分解和复合，易于分析，这样的 系统是库所、变迁和予系统的集合。同样弥补了普通p e t r i 网没有数据概念和无层次概念 的不足。文献 1 5 用分层p e t r i 网对w s b p e l 的流程进行建模，并用工具h p s i m 对 w s b p e l 流程进行分析与验证。 时延断言p e t r i 网( t i m e dp r e d i c a t ep e t r i n e t ，t p p n ) 也是普通p e t r i 网的扩展。文献 2 9 ，用t p p n 建模w s b p e l 过程中，考虑到了与时问有关的信息，定义了从变迁集合 到某种时间因素的映射。并对服务组合的可达性、安全性、活性进行分析，并从t p p n 网的理论对这些性质进行了分析，相应的验证工具m c t 4 w s 正在开发中。 2 3 建模w s b p e l 活动的典型方法一自动机理论 1 9 3 6 年英国数学家a m 图灵提出种抽象自动机，称为图灵机，用来定义可计算 函数类，开创了自动机的抽象理论。在自动机理论中，自动机都是指抽象计算模型，即 能变换和处理信息的离散系统的动态数学模型【3 0 1 。 1 业务流程自动机 为了用有限状态自动机来描述服务，下面给出业务流程有限状态自动机的定义【3 2 j ： 业务流程的有限状态自动机( f i n i t es t a t ea u t o m a t a ，f s a ) 是一个五元组( q ，万，q o ，f ) ， 其中： 第_ 二章相关研究 驴 q o , q t q 月 是一个有穷的状态集合，表示在任一确定的时刻有限状态自动机只能处于 一个确定的状态q i ： = q ，哆，a m ) 是一个有穷集合，是业务流程的字母表，表示流程中原子活动集合； 万：q _ 9 是状态转移函数，在某一状态下执行一个活动后，业务流程将转入由状态 迁移函数决定的一个新的状态； q o eq 是起始状态，有限状态自动机由此开始接收输入活动； f q 是接收状态集，有限状态自动机在达到终态后，业务流程的执行终止。 2 基于自动机的建模与验证原理 一个状态转移系统对应着一个自动机模型。将实际系统的状态定义为自动机模型中 所有的状态变量全部的取值。有限状态自动机就可以对这些有限状态系统进行建模，并 用模型检测方法，将所有验证的属性用一条时序逻辑语句来表达，即状态迁移系统s 是 否是模念时态公式f 的一个模型【3 i 】。 依据对b p e l 结构化活动的状态迁移分析，业务流程的行为表现为一系列状态的迁 移。状态的迁移由活动的执行激发，因此在明确了各个活动的执行状态以及状态之间关 系的基础上，可以用自动机模型来表示业务流程的行为。 3 有限状态自动机对w s b p e l 活动的建模【3 2 1 在w s b p e l 中，表示流程的开始，转换到状态图中，即表示一个状态机 仁( q ，吼，a ，m ，万) 。 在w s b p e l 中，p a r t n e r 用来表示流程中不同的参与者，在d f a 中，不需要建 模。 元素，在d f a 中被建模为消息类型，即。 在w s b p e l 中表示接收一个消息。在d f a 中，增加两个状态吼，q i + l ，同时增 加状态转移函数万( 吼，m ) = q ，+ l ，m 为c o n t a i n e r 中对应的消息类型，方向取值为“+ ”。 活动表明发送一个消息。在d f a 中，增加两个状态q ，q 川，同时增加状态转移函 数6 ( q ，m 。) = q ，+ l ，m 为c o n t a i n e r 中对应的消息类型，方向取值为。 是一个同步操作，对应着输入，输出两个信息。在d f a 中，增加三个状态 研，吼+ l ，吼+ 2 ，同时增加状态转移函数万( 9 f ，m ) = q + i ，m + i n m ，6 ( q ，+ l ，m ) = q f + 2 ，m t _ 1 2 两北大学硕一l 二学位论文 o u tm 中对应的减盆。 元素的作用是更新容器值，只是内部动作，不涉及状态转换，转换被忽略。 元素是抛出异常，在d f a 中，没有相应元素，转换被忽略。 元素终止业务流程，在d f a 中，增加终态f ，q = qu t 。 4 自动机理论建模w s b p e l 活动的研究成果 随着自动机理论的发展和应用的需要，许多新( 或变型) 的自动机模型被提出并进行 了深入的研究。有限状态自动机是自动机理论最基本计算模型之一。它拥有有限数量的 状态，每个状态可以迁移到零个或多个状态，输入字符串决定了哪个状态的迁移。时间 自动机、袋自动机【3 3 】、接e l 自动机、e f a 等都是对有限状态自动机的扩展，有效增强了 它的描述能力。本文所介绍的研究成果都是基于有限状态自动机。 文献 1 9 详细介绍了d f a 建模w s b p e l 活动详细过程，文章所做的工作是验证任 意两个协议是否兼容、是否是可替换的。文献 3 4 用接口自动机形式化描述w s b p e l 的相关活动，采用接口自动机在描述w e b 服务组合异步交互存在不足。文献 3 5 介绍 了一种从b p e l 的应用程序中抽取业务流程的行为并用e f a ( e x t e n d e df i n i t e s t a t e a u t o m a t o n ) 扩展的有限自动机来描述。并将e f a 转换成p r o m e l a 源程序，用s p i n 模型 检测工具进行验证。文中提供的转换算法能避免死锁的发生，而且能分析b p e l 规范中 四个应用实例。 目前用自动机理论建模w s b p e l 主要问题有映射规则不完全，且建模后存在状态 空间爆炸。 2 4 建模w s b p e l 活动的典型方法一进程代数理论 进程( p r o c e s s ) ，在计算机领域指的是应用程序的一次执行过程。相对于静态存在的 应用程序，进程是动态存在的。它指的是系统的行为。系统是展示行为的系统，特别是 一个软件系统的行为。行为是一个系统执行的动作或事件的总和，这些动作或事件的执 行可能是定时的或随机的。“代数”一词指用代数的或公罩的方法讨论行为。所以，进程 代数式用代数的方法研究系统行为的一门学科。 1 进程代数( p r o c e s sa l g e b r a ) 进程代数是一种形式化地描述复杂并发系统的建模工具，是一种高层的描述语言， 是支持并发分布系统的组合描述和其性质形式化证明的代数语言。它以代数形式来描述 1 3 第一二章相关研究 模型，并为模型化系统定义了一套完整的语法和语义。 进程代数的共同特征为： 1 ) 均使用通信，而不是共享存储，作为进程问相互作用的基本手段，表现出面向分布 式系统的特征。 2 ) 语法上，用一组算予作进程构件。算子语义用结构化操作语义( s o s ) 方法定义。进程 可看成标号迁移系统( t l s ) 。 3 ) 把并发性归结为非确定性，将并发执行的进程的行为看成是各个进程的行为的所有 可能的交错合成，即所谓的交错式语义。 进程代数 进程代 数l j ：具 b p e l 文件 个 专冷 输入输入i 输入 c a d pc w b n cm w b q 小 l 死锁ll 活锁h 互模拟 模 型 转 换 性 质 检 验 图2 7 进程代数( p a ) 和进程代数工具( p a t ) 图2 7 列举了三种不同的进程代数模型及其对应的验证工具，c c s 因其概念简洁， 可用的数学工具丰富，在并发系统的规范、分析、设计和验证等方面获得了广泛应用。 所以本节主要介绍c c s 最基本的部分： p ：= 0a pp + qpi iqa ( x ) a - - = a ? ( x ) i 口! ( x ) if 其中0 表示不含任何变换的操作； 前缀操作：n 尸表示先执行a ，再执行进程j p 操作。 选择操作：p + q 表示不确定选择，要么执行p 要么执行q 。 并发操作：e l q 表示同时执行尸和q 执行，“i l ，表示并行组合。 口? ) 表示通过端口a 接收工消息。 1 4 两北人学硕1 ：学位论文 口! ( x ) 表示在端口a 发送消息x 。 r 是指的外部看不到的内部动作。 2 基于进程代数的建模与验证原理 进程代数的表达能力强且形式简洁，它通过进程迁移图细致的表达系统的交互行 为，根据结构化操作语义和系统的约束条件得到进程表达式。用进程代数提供的丰富验 证工具进行验证，尤其含有成熟的等价理论，为验证服务组合的兼容性、等价性提供了 良好的理论基础。 w s b p e l 中活动表达的涵义是固定的，由于前文已有对活动的简单介绍，这里就 不再赘述，直接