（计算机软件与理论专业论文）一种基于mealy机的bpel程序验证模型研究.pdf

西南大学硕十学位论文 摘要 曼曼! 皇曼曼曼量曼曼曼曼曼曼量舅舅曼曼曼曼曼曼曼曼苎! ! 曼量皇皇曼曼曼曼! ! 曼曼曼曼蔓曼曼曼曼曼曼曼曼曼曼蔓曼曼曼曼曼曼曼鲁! ! 曼曼量量皇曼曼皇曼曼 一种基于m e a ly 机的b p e l 程序验证方法研究 计算机软件与理论专业硕士研究生闻晓 。 指导教师张为群教授 摘要 b p e l 作为描述w e b 服务编制的语言之一，在商业流程中被用来描述活动和对活动的控 制。b p e l 具有类似程序设计语言的语法结构，如顺序、分支和循环等，能表达对业务流程的 控制。b p e l 语法中还有专为商业流程设计的结构，兼顾了i t 和商业两个领域的需求。但是 这给b p e l 程序验证带来了难题。b p e l 不是一种可执行的程序语言，往往冗长而复杂，仍然 存在二义性、不一致性和不完备性。为了提高w e b 服务中b p e l 应用程序的健壮性，有必要 改进程序验证的方法。 本文对现有基于模型检测技术的b p e l 程序验证方法进行了研究，提出了一种基于m e a l y 机的验证模型b v m ( b p e lv e r i f i c a t i o nm a c h i n e ) ，并利用该模型建立了一个验证b p e l 程序 性质的方法。本文通过已知b p e l 程序源码找出验证程序需要的b v m 模型m 和通过用户需 求说明书找出待验证的性质p ，设计并实现了一个在模型检测器n u s m v 中验证m 是否满足p 的引擎。实验显示该方法能够验证包括补偿的b p e l 程序，弥补了现有方法在这方面的不足。 关键词：b p e l 模型检测w e b 服务w e b 服务编制 西南大学硕士学位论文 a b s t r a c t ab p e l p r o g r a m v e r i f i c a t i o nm e t h o dr e s e a r c h ba s e do nm e a l ym a c h i n e m a jo r ：c o m p u t e rs o f t w a r ea n dt h e o r y s p e c i a l t y ：s o f t w a r ee n g i n e e r i n g 一一 一 一 s u p e r v i s o r ：p r o f z h a n gw e i q u n a u t h o r ：阢nx i a o a bs t r a c t a so n eo ft h ed e s c r i p t i o nl a n g u a g e si nw e bs e r v i c eo r c h e s t r a t i o n ，b p e li su s e dt os t a t et h ea c t i v i t i e s o fb u s i n e s sp r o c e s sa n dt h ec o n t r o l st oa c t i v i t i e s t h e r ea r es o m es y n t a xs t r u c t u r e sl i k ec o m m o n p r o g r a ml a n g u a g e si nb p e lw h i c hc a l ld e m o n s t r a t et h ec o n t r o l st ob u s i n e s sp r o c e s s ，c g ：s e q u e n c e ， b r a n c ha n dl o o p s p e c i a l i z e ds t r u c t u r e sa r cd e s i g n e df o rb u s i n e s sp r o c e s st om e e tt h er e q u i r e m e n t b o t hf r o mi ta n db u s i n e s sd o m a i n h o w e v e r , i t b r i n g ss o m ep u z z l e si nv e r i f y i n gb p e lp r o g r a m s b p e li sn o ta ne x e c u t a b l el a n g u a g e ，w h i l ew i t hp r o l i xa n dc o m p l i c a t e dc o d e si tu s u a l l ys u f f e r sf r o m a m b i g u i t y , i n c o n s i s t e n c ya n di n c o m p l e t e n e s s i ti sn e c e s s a r yt oi m p r o v et h em e c h a n i s m o fv e r i f y i n g b p e l p r o g r a m i no r d e rt or e i n f o r c et h er o b u s t n e s s t h i sp a p e rd e a l sw i t ht h er e s e a r c ho nt h ev e r i f i c a t i o nm e t h o do fb p e lp r o g r a mb a s e do nm o d e l c h e c k i n gt e c h n o l o g y , a n dp r e s e n t sav e r i f y i n gm o d e lb a s e do nm e a l ya u t o m a t a b v m ( b p e l v e r i f i c a t i o nm a c h i n e ) w h i c hi sa d o p t e dt oc o n s t r u c tam e t h o da i m e da tv e r i f y i n gt h ep r o g r a m p r o p e r t i e s b yf i n d i n go u tt h er e q u i r e db v m m o d e lmf r o mt h ek n o w nb p e ls o u r c ec o d ea n d p e n d i n gp r o p e r t i e spf r o mu s e rs p e c i f i c a t i o n , t h ep a p e rd e s i g n sa n di m p l e m e n t sa l le n g i n ei nm o d e l c h e c k e rn u s m vt ov e r i f yw h e t h e rm s a t i s f yp t h ec a s es t u d ys h o w st h a tt h ea b o v em e t h o d sa r e a b l et ov e r i f yt h eb p e l p r o g r a m si n c l u d ec o m p e n s a t i o n ，f i l l i n gu pad e f i c i e n c yo fc u r r e n tm e t h o d s k e y w o r d ：b p e lm o d e lc h e c k i n g w e bs e r v i c ew e bs e r v i c eo r c h e s t r a t i o n 独创性声明 本人提交的学位论文是在导师指导下进行的研究工作及取得的研 究成果。论文中引用他人已经发表或出版过的研究成果，文中已加了 标注。 学位论文作者：2 鹬啪 签字日其】9 ：研年厂胪歹日 学位论文版权使用授权书 本学位论文作者完全了解西南大学有关保留、使用学位论文的规 定，有权保留并向国家有关部门或机构送交论文的复印件和磁盘，允 许论文被查阅和借阅。本人授权西南大学研究生部可以将学位论文的 全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫 描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书，本论文：口不保密， 口保密期限至年月止) 。 学位论文作者签名：闻啪 签字日期： 矽7 年歹月矽日 西南大学硕士学位论文第1 章绪论 曼曼曼舅皇量皇量詈曼皇蔓曼曼蔓曼皇曼i i i 一一一i ii 一 一 一一一 i 曼曼曼 第1 章绪论 1 1研究背景 互联网的热潮推动了w e b 服务的出现和发展，商业执行过程中的软件越来越多的表现为 w e b 服务。随着“s a a s ”( 软件即服务) 这种通过互联网提供软件模式的引入，用户逐渐从购 买软件转变为向服务商租用软件服务，并且服务商将同时提供软件今后的维护服务。于是，用 户的关注重点将从单个w e b 服务，逐渐转移到服务的组合或者编制。多个w e b 服务可以互相 协作来提供单个w e b 服务很难达到的功能。b p e l 就是一种应运而生的描述w e b 服务组合的 语言。它既提供了丰富的语法结构来表达商业执行过程中节点之间的转换关系，也在语言的 语义方面适当降低了形式化的程度。众所周知，一位商业领域专家比程序员更熟悉商业业务。 那么如果这位专家使用b p e l ，将能更容易地、更准确地描述业务执行过程。然而非形式化的 b p e l 不能直接在计算机上编译后运行，这给验证b p e l 程序的正确性带来了困难。b p e l 所 描述的商业执行过程往往涉及跨越几千公里的地理范围，并包含几小时甚至几天的时间间隔。 代码的这种复杂性使得运行前验证变得十分必要。近年来，化解b p e l 程序验证矛盾的方法正 在成为研究热点，基于模型检测技术的方法就是其中代表之一。 1 1 1w e b 服务的编制 w 曲服务的组合有两种模式：一种是w 对等”模式( w e bs e r v i c ec h o r e o g r a p h y ，简称编 排或者w s c ) ，协作的各方通过公共消息交换来完成业务交互；另一种是“集中”模式( w 曲 s e r v i c eo r c h e s t r a t i o n ，简称编制或者w s o ) ，协作的各方听从全局“指挥者”的安排来完成业 务交互。w s o 为组成编制的服务作了定义，以及制定这些服务的执行顺序( 比如顺序、并行、 条件分支逻辑等) 。因此可以将编制视为一种比编排简单的流程，这种流程自身也是一个w e b 服务，流程的控制权由“编制设计者”集中管理。w s o 通常包括分支控制点、并行处理选择、 人类响应步骤以及各种类型的预定义步骤( 例如转换、适配器、电子邮件及w e b 服务等) 。实 现业务流程的运行时生命周期需要执行多个活动。b p e l 是一种w e b 服务编制语言，不同于 流程编排。流程编排可描述多个贸易伙伴为了实现多组织业务功能而进行的交互。例如，在 供应链方面，实施产品采购可能涉及到多家公司的定单、发货通知单和资金的交互。编排不 描述每个公司如何处理操作，只描述不同公司如何彼此交互。流程编制使用一个中心流程来 协调不同的w e b 服务操作。这个中心“指挥家”( 就像在管弦乐团一样) 了解编制的总体目 标、涉及的操作以及操作的调用顺序。这种集中化管理使w e b 服务能够在不了解彼此影响的 情况下进行添加和删除，还允许在出现错误和异常的情况下进行补偿。流程编制和流程编排 仅在描述服务接口和交互方面类似。对本文而言，我们将关注流程编制。当使用b p e l 进行 编制时，b p e l 语言将提供一个标准来控制整体操作序列、调用服务以及在b p e l 服务器上 执行。 1 1 2验证b p e l 程序的意义和挑战 b p e l 最初是在2 0 0 2 年7 月随同b p e l 4 w s l 0 规范的发布而出现的n 1 ，是m m 、m i c r o s o f t 1 西南大学硕士学位论文第1 章绪论 和b e a 合作的成果。它结合并且替换了i b m 的w e bs e r v i c e sf l o wl a n g u a g eo v s f l ) 和微软公 司的x l a n g 规范。b p e l 是一种基于x m l 的描写业务流程的编程语言，被描写的业务流程 的每个单一步骤则由w e b 服务来实现。b p e l 的目标是要实现业务流程定义格式的标准化， 使得公司之间可以通过w e b 服务无缝的进行交互。在企业内部，b p e l 用于标准化企业应用 程序集成以及将此集成扩展到孤立的遗留系统中。在企业之间，b p e l 使与业务合作伙伴的集 成变得更容易。b p e l 激发企业进一步定义自身业务流程，从而导致流程的优化、重新设计以 及选择最合适的流程。b p e l 中描述的业务流程定义并不影响现有系统，因此简便了升级过程。 在已经或将要通过w e b 服务公开功能的环境中，b p e l 是一项重要的技术。 、 b p e l 全称为w s b p e l ，w s b p e l 原名b p e l 4 w s ，最初是在2 0 0 2 年7 月随同 b p e l 4 w s l 0 规范的发布而出现的。业务处理执行语言结合并且替换了m m 的w 幽s e r v i c e s f l o wl a n g u a g eo v s f l ) 和微软公司的x l a n g 规范。随着s a p 和s i e b e ls y s t e m s 等其它贡献者 的加入，b p e l 4 w s 规范的l - l 版于2 0 0 3 年5 月发布。该版本获得了较多的关注与厂商的支 持，这导致产生大量的商业上遵循b p e l 4 w s 的可用编排引擎。o a s i s 随后宣布将语言本身 重新命名为w e b 服务业务流程执行语言( w s b p e l ) ，并于2 0 0 7 年4 月1 2 日正式发布 w s - b p e l 2 0 规范，将其作为一个官方的、开放的标准。 b p e l 应用程序本质上是基于工作流模型的设计。而工作流的描述涉及到分布式环境中众 多的并行协作过程。一般来说，编写b p e l 程序前应当比较了解相关w 曲服务的领域背景知 识，这样才能高效地寻找w e b 服务的接口定义( w s d l ) 和合作伙伴之间的协作链接类型。 然后才开始编写b p e l 流程的逻辑定义。正是因为上述过程繁杂而耗时，使得编写b p e l 十分 不易，程序运行后往往遇到与并行处理相关的问题，例如进程交互中的“死锁”问题。尽管 b p e l 专门针对商业执行过程的环境而设计，但是它在语义上仍然存在二义性、不一致性和不 完备性的缺点。因为b p e l 并不能直接在计算机上运行，所以常见的程序测试方法对于验证 b p e l 程序的正确性并不奏效。对b p e l 的进一步形式化能够减少上述缺点，并能对b p e l 过 程的推理、开发和验证起到促进作用。近年来，o a s i s 组织的w s b p e l 技术委员会一直致力 于b p e l 的形式化工作。建立b p e l 的形式化模型并加以分析，有助于在运行前侦测程序错误。 实现上述过程的工具能够有效提高b p e l 程序验证的效率。 1 1 3b p e l 语言的补偿事务 在全球化浪潮的影响下，国与国之间的商业合作日益频繁。商业执行过程在时间和空间 上得到了极大的扩展。一次商业执行过程可能包含上百个异步执行的应用节点，如果其中一 个应用发生错误，对它有依赖关系的应用可能已经开始执行。补偿旨在允许对无法参与事务 的系统应用反向操作，或者在已经决定系统不应作为事务的一部分进行操作时应用反向操作。 例如，一个w e b 服务可能允许递减库存，但一个错误使其必须回滚流程。在这种情况下，补 偿处理程序应定义为调用w e b 服务递增库存，从而有效地提供了一个反向事务。补偿是指还 原已经完成的活动，使得流程中已经运行完成的所有活动都会依照预设的逻辑进行恢复。 b p e l 语言允许使用w e b 服务组件开发复杂的商业执行过程，简称业务流程或者b p e l 流程。b p e l 流程可指定调用哪些w e b 服务以及调用的顺序。b p e l 服务器跟踪事务中涉及 的业务流程，确保这些步骤以正确顺序执行，并管理事务、补偿和异常。b p e l 支持来自任何 2 西南大学硕士学位论文第1 章绪论 1 i i i 曼鼍皇寰皇曼曼曼寰曼量鼍曼鼍曼曼曼曼曼曼曼曼舅曼曹曼曼皇曼曼皇曼曼曼鼍曼皇曼曼曼曼曼曼鼍曼曼皇曼曼! 曼曼曼曼 编制语言的控制流结构：循环和条件、变量，分配数据值，定义错误处理程序等等。b p e l 接 收活动用于为客户端创建一个业务流程实例的事件或消息，i 然后该流程将调用已定义的业务 流程序列中的其他服务。通常，该调用将生成一个响应或者回复。其中，b p e l 流程可能必须 操作数据变量( 赋值) ，处理错误和异常( 引发) 或等待一段时间。变量被用来定义在整个流 程描述中使用的所有消息和数据。变量用于发送到涉及的服务或从它们接收的每个消息，它 们用于与任何编程语言相同的方式处理流程执行。结构化活动可能包括按顺序( 序列) 执行 活动或并行( 流) 执行活动的b p e l 编制。由此可见，b p e l 语言在结构上具有和其他编程 语言类似的特征。 b p e l 处理编制服务中使用伙伴链接( p a r m e r l i n k ) 这个概念，它为该流程与之交互的各方 定义接口，客户端通过该接口调用b p e l 流程自身。这些伙伴链接连接了b p e l 流程和该接 口调用的服务。b p e l 流程灵活绑定到物理服务端点，可以在设计、部署或运行时进行。 b p e l 具有对异步事件的处理功能。b p e l 流程可以在任何时候等待，以便从客户端接收 消息或请求。b p e l 引擎将处理保持流程状态的开销，直到该消息传入并将消息与特定流程实 例相关联。b p e l 流程自身可将同步或异步接口公开给它们的客户端。同步b p e l 流程操作 会锁定客户端直到流程返回对客户端的响应。异步b p e l 接口可以是单向的，或通过回调返 回对客户端的响应。异步流程常用于较长期运行的操作，而同步常用于较短期运行的操作。 b p e l 中专门为补偿事务设计了语法结构，可以用来增强语言的表达能力，适应了异步条 件下耗时较长的操作的需求。通常情况下，实现有用的业务流程用例( 当一切准备就绪时) 只是业务流程总体设计和实现工作的其中一部分。大部分时间都花费在定义所有适当的异常 处理逻辑上，以便构建在所有预期条件下( 甚至在意外条件下) 能够进行合理操作的强健且 灵活的流程。b p e l 提供了丰富的异常处理功能，以便开发人员可以定义( 以分层t r y c a t c h 类 型模式) 在流程执行过程中出现异常和错误时如何处理。但是，除了异常处理之外，一些流 程需要更具事务性的行为。在短期流和服务方面，标准事务模型足够用了，因为它们使用的 是x a 或a c i d 事务模型，其中的资源可在事务持续时间内锁定并在必要时回滚。但是，在 业务流程编制领域，服务可能由外部组织拥有，并且执行流程和服务接口可能要花几分钟、 几小时甚至是几天，因此需要一个新的事务模型，称为长期运行的事务或补偿事务。虽然该 领域正等待这方面实际标准的颁布，以便允许事务协调器自动处理补偿事务，但是b p e l 语 言通过一个称为补偿处理程序的特性为该功能提供了支持。 补偿处理程序可以显式撤销在某个错误生成前成功完成的工作。每个调用活动可以按需 与撤销它的补偿活动配对。如果出现错误，针对在失败活动范围内已经完成的工作的补偿处 理程序将用于撤销完成的工作。不足之处在于，该补偿处理程序方法需要流程设计器显式地 考虑如何补偿每个活动。b p e l 引擎将在运行时跟踪所有活动并只为以前完成的步骤执行那些 补偿处理程序。此外，b p e l 引擎将在运行时对数据进行快照，以便补偿处理程序在初始活动 完成时可以访问当前数据。该方法意味着服务自身无需具有对补偿事务的显式支持，因为对 补偿事务而言仍然没有诸如x a 和j t a 的标准。 1 1 4基于模型检测技术的验证方法 研究表明，模型检测埋1 ( m o d e lc h e c k i n g ) 特别适合验证交互的进程中与并行通信相关的 3 西南大学硕士学位论文第1 章绪论 性质旧1 。与其他验证技术相比，模型检测的鲜明特点是简洁明了和自动化程度高。e d m u n dm c l a r k e 等人在并发系统性质方面的研究工作为自动验证方法开辟了一条新的途径，成为近二十 年来计算机科学基础研究的一个热点。模型检测已被应用于计算机硬件和通信、安全认证等 协议方面的分析与验证中，在学术界和产业界均取得了举世瞩目的成功。 早期的模型检测侧重于硬件设计的验证，因为这类验证过程中涉及的状态未能给模型检 测算法带来大多困难。对于复杂的协议和软件，系统状态可能是无穷的，这促使验证技术倾 向于抽象和简化的方法。于是，严格说模型检测在这一领域并非能像硬件设计验证一样完备。 但检测的结果对于协议和软件的分析依然大有裨益。随着研究的进展，模型检测的应用范围 逐步扩大，涵盖了通讯协议、安全协议和软件某部分。 模型检测算法对系统状态空间进行穷举地搜索。对于并发系统，其状态的数目往往随并 发进程数量的增加呈指数增长。对于软件系统也有了类似现象。用k r i p k e 状态转换图直接存 储系统模型的状态和状态转换关系，当系统状态数目很大时，往往不可避免地会出现状态爆 炸的问题，导致内存不足而中断验证过程。因此系统空间状态较多时，穷举地搜索是不可行 的。对于以上这类所谓的状态爆炸问题，符号模型检测的基本原理h 1 是将系统的状态转换关系 用逻辑公式或布尔函数表示，状态集合的运算被转化为布尔函数的运算。二叉图( b i n a r y d e c i s i o nd i a g r a m ) 是用来表示布尔函数的重要手段，它能较为紧凑地表示状态转换关系，以 达到降低系统模型所需的内存空间的目的。由此可见，对于一种基于模型检测技术的验证方 法来说，合理地控制系统状态空间对其可用性至关重要。 模型检测技术中，主动降低验证系统空间规模的探索一直在进行。“o nt h ef l y 模型检测” 的思想是事先预判系统执行路径，只生成路径中所包含的状态，避免验证系统中包含的所有 状态。一个系统可由多个进程组成，一次并发执行过程中，不同进程的动作可以有许多不同 的次序，但是可能有相同的结果。于是可以将某些状态的次序固定，以减少重复验证本质上 相同的路径。这就是偏序归约模型检测的思想。此外，多进程组成的系统中某些进程可能完 全类似，并发执行的结果可能产生许多相同或相似的路径。于是可以搜索一次具有对称关系 的进程执行路径，以避免重复搜索对称或相同的系统状态。这就是对称模型检测的思想。 模型检测器是用来进行模型检测的工具或者程序。验证之前既需要为待验证的系统建立 模型，还需要对待验证的性质进行形式化的表示。对于有穷状态系统，以上的模型是否满足 性质的问题是可判定的。目前较为著名的模型检测器有n u s m v 、s p i n 等。在验证结束时， 模型检测器都能给出明确的结果，并且对于未满足的性质给出一个反例。 目前流行的模型检验器基本上都有自己的系统描述语言。模型检验器种类很多，各自偏 向软件或者硬件验证，例如s p i n 、s l a m 、j a v ap a t h f i n d e r 、用于控制系统的u p p a a l 、基于符 号模型检测的n u s m v 、基于p e t r i 网的p r o d 以及检查c 代码的m o p s 等等。由于适用范围 不同，本文选择了n u s m v 。美国卡内基梅隆大学的l m c m i l l i a n 博士于1 9 9 2 年开发出了的模 型检测器s m v ，它基于“符号模型检验”( s y m b o l i cm o d e lc h e c k i n g ) 技术。设计s m v 的初衷 是主要为了研究符号模型检测应用前景，开发一种对硬件进行检测的工具。到现在s m v 应经 成为世界上广为流行的分析有限状态系统的常用工具之一，最新版本是n u s m v 2 4 3 膳1 。系统 模型用s m v 语言描述哺，一个s m 、r 程序由两部分组成：一个有限状态转换系统和一组c t l 公 式。s d 4 v 把初始状态和转换关系表示成二叉树图b d d s ( b i n a r yd e c i d i n gd i a g r a m s ) ，性质也就是 4 西南大学硕士学位论文第1 章绪论 c t l 公式，也表示成b d d s ，通过模型检测算法搜索系统状态空间，给出结果：一个声明的性 质是正确的；或者是不正确的，并给出一个不满足这个性质的反例( 也就是从初始状态开始的 一系列状态) 。一个c t l 公式的真值通过遍历状态图的方式确定，这种遍历的时间复杂性和状 态空间大小、公式的长度成线性关系。 本文选择n u s m v 作为研究的辅助工具，除了以上显示的n u s m v 是一个成功的模型检测 工具，能够对大规模的软件包进行检验以外，还包括以下原因： 1 )n u s m v 适用范围广，与软件的运行平台无关。 2 ) n u s m v 工具是开源的，源代码可以从网站h t t p ：n u s m v i r s t i t c i t ，上免费获取，可以 更容易地了解其实现方面的细节，使得对深入研究验证的过程、改进验证方法变得 可能。 3 )n u s m v 是一个轻量级的模型检测工具，只是抽象出程序的控制流图，不需要数据流， 可以为系统减少内存空间。 1 2 国内外研究现状 对b p e l 程序进行建模并验证的方法非常多，主要区别在模型的选取上。p e t r i 网、有限 自动机、进程代数等都有被学者用来建立b p e l 程序的模型。其中具有代表性的基于有限自动 机模型的验证方法如下。 j a n ak b o l l l 一刀提出了对面向业务专家的流程模型进行转换的必要性，并对转换过程添加 了限制性条件。即转换前的流程规格必须是无二义性的，并且转换后的模型能够被计算机自 动化验证。j a mk e o h l e r 仅仅对b p e l 在业务执行过程中常用的结构模式进行了转换，原因在 于他将建模与验证间隔为两个阶段，分别由业务领域和计算机领域各自的专家负责。选取常 用的结构模式来验证便于整个验证中不同角色专家间的交互，但验证的范围存在局限性。 s h i nn a k a j i m a t 8 】将b p e l 程序转换为有限自动机模型，在s p i n 中验证了b p e l 程序中流 程的可达性以及程序运行中应当满足的性质。验证中采用的自动机模型不仅清晰地描述了业 务执行过程中活动的行为规格特征，还将需要验证的性质用自动机表现了出来。s h i n n a k a j t m a 的研究成果中还增加了其他方法较难完成的验证d p e ( d e a d p a t he l i m i n a t i o n ) 的部分，但未 能验证b p e l 中同样重要的补偿部分。 y o n g y a nz h e n g 9 1 等人提出的w s a 模型捕获了b p e l 中的操作语义，给出了生成测试用例 的框架。w s a 模型不仅能对业务执行过程中的数据流进行分析，也能描述处于交互状态中的活 动。v b r b u s 是一个模块化、可扩展的自动化业务过程验证工具。它的核心架构采用三层结 构：设计层、形式化层和验证层。形式化层是业务过程的规格或定义，它给设计层和验证层 各自的描述语言搭起了“桥梁”。v e r b u s 的远景目标是将设计层涵盖的各类语言转换为统一 的模型，并在接下来的验证层中可以选用不同的验证工具。 通过研究现状可知，当前对b p e l 程序建立模型并验证性质的方法重点在模型选取和验证 范围上。验证目标的差异可能对这两点产生很大影响u 训。补偿本身就是商业业务领域中保证 各方利益均等的要素之一，也是b p e l 中提高业务执行过程描述能力的重要结构模式。通过与 自动机模型的对比分析发现，补偿的运行机制与自动机中转移函数具有类似之处。于是利用 自动机模型描述b p e l 中补偿结构，并以此来验证补偿中涉及的性质，具有重要的现实意义和 5 两南大学硕士学位论文第l 章绪论 可行性。 1 3 研究目的和内容 本文对现有的基于模型检测技术的b p e l 程序验证方法进行了研究，发现如何全面地验证 b p e l 程序一直是很难解决的问题。作者试图寻找一种方法，它能验证包括补偿行为在内的 b p e l 程序，同时使得验证方法具有可行性、结果具有真实性。 因此作者提出了一种描述b p e l 程序的b v m ( b p e lv e r i f i c a t i o nm a c h i n e ) 模型，并建 立了基于此模型的验证方法。首先以m e a l y 机为基础建立了b v m 的形式化定义。然后构建了 b p e l 中结构活动与b v m 定义中各部分的映射关系。特别是利用了有限自动机中转移函数来 分析补偿行为中活动的关系。最后编写了转换b p e l 成为b v m 的算法，并依据转换后的b v m 调用模型检测器进行验证。末尾在实例中进行了探讨。 1 4 预期结果 本文致力于验证b p e l 程序中与补偿行为相关的性质，弥补现有方法在这方面的不足。本 文的方法预期有以下几点结果： 1 )为定义了补偿行为的b p e l 程序建立一种b v m 模型。 2 )建立一种通过n u s m v 模型检测器验证b v m 模型性质的方法。 3 )使用第二步中的方法对一个b p e l 程序软件开发案例进行验证分析，并显示出该方法 在发挥软件验证作用方面的优越性。 1 5 本文组织结构 论文的后续章节分别为： 第2 章基本理论，主要介绍本文研究涉及的理论基础，包括b p e l 语言、模型检测、有 限自动机和时态逻辑。 第3 章模型构建，主要介绍b v m 模型的定义和建立的方法 第4 章模型验证，主要介绍通过模型检测器验证b v m 模型的方法 第5 章案例研究，简要展示一个经典案例的开发过程，并分析此案例的b v m 模型，将 生成的验证结果反馈给开发者。 第6 章对本文研究进行总结。 6 西南大学硕士学位论文第2 章基本理论 第2 章基本理论 2 1b p e l b p e l 是b u s m e s sp r o c e s se x e c u t i o nl a n g u a g e 的缩写，意为业务过程执行语言，是一种基 于x m l 的、。用来描写业务过程的编程语言，被描写的业务过程的每个单一步骤则由w e b 服 务来实现。b p e l 程序代码基于w s d l 建立的文档，此外它还使用x m l 模式定义、x p a t h 和 w s a d d r e s s i n g 等标准。b p e l 也曾经被称作w s b p e l 和b p e l 4 w s 。b p e l 、w s b p e l 和 b p e i a w s 之间除了历史参考文献不同外，没有什么其他的不同。这些名字都涉及到相同的待 定标准。“b p e l 4 w s ”是起初规范的名字。m m 、b e a 和微软于2 0 0 2 年一起开发和引入了 b p e l ，作为描写协调w e b 服务的语言。w s b p e l ”目前是规范和待定标准的名称。当这个 规范提交到o a s i s 时，出于w e b 服务相关标准的努力，按照o a s i s 命名方案更换了这个名 字。尽管如此，大部分团体仍然简单地称这个标准为“b p e l ”。 现代企业的发展和规模的扩大，企业信息及资源已呈现出异构分布和松散耦合的状态， 原有集中式的模式已不能满足日益增长的事务处理、信息处理和决策支持等方面的要求。随 着计算机技术的发展和i n t e m e t 的广泛应用，工作流技术越来越受到人们的重视。工作流技术 是一项为达到协同工作环境而进行人与人、人与部门、部门之间信息的分类、共享、交换、 组织和协调的技术。因此工作流管理系统的功能由最初的无纸化办公，转变成为简化企业复 杂信息环境，实现企业业务流程自动化的工具。 高效的业务流程是企业一贯追寻的目标。业务流程管理( b p m ，b u s i n e s sp r o c e s s m a n a g e m e n t ) 成为企业管理前沿和研究热点。随着全球化竞争的日趋激烈，企业成为快速响应 的流程企业的要求日益迫切。b p m 旨在利用i t 技术建立一种贯穿于整个企业流程生命周期的 管理机制，以使业务流程可分析、可管理、快响应、易变更。 b p e l 是一门用于自动化业务流程的语言。用x m l 文档写入b p e l 中的流程能在w 曲服 务之间以标准化的交互方式得到精心组织。这些流程能够在任何一个符合b p e l 规范的平台或 产品上执行。企业的业务流程涉及企业的众多资源，包括数据，应用程序，e r p 软件，供应链， 人员等，如果要对企业现有的资源进行全新的改造，必然要付出昂贵的代价，而且以前的投 资也将付之东流。所以，b p e l 通过允许企业在各种各样的创作工具和执行平台之间移动这些 流程，有能力对现有资源进行整合，最大限度的利用现有资源，对它们进行很少的改造或根 本不用修改就能集成到业务流程系统中来。这样企业节省了流程自动化上的原有成本。尽管 业界以前想使业务流程定义标准化，但b p e l 已经引起了史无前例的兴趣，而且它最早在软件 供应商中获得大量认可。 b p e l 结合了基于图形的流程语言和基于块结构的流程语言的优点，提供了描述业务流程 的定义语言，描述了业务相关的时间、顺序、地点等内容。b p e l 基于w s d l1 1 、x m l s c h e m a l 0 和x p a t h l 0 规范。其中，w s d l ( w e bs e r v i c ed e s c r i p t i o nl a n g u a g e 。w e b 服务描述语言) 消 息和x m ls c h e m a 类型定义提供了b p e l 流程所需的所有数据模型。而所有需要的外部资源 和伙伴( 业务流程交互的服务被模拟成伙伴) 都被描述为w s d l 服务。w s d l 使用抽象消息 来定义抽象功能，服务的用户必须静态地依赖于这种抽象接口。b p e l 依赖并扩展了原始的 w s d l l 1 规范，遵循该规范在抽象接口关系和具体部署描述信息之间的区分原则，增加了合 7 西南大学硕士学位论文第2 章基本理论 作伙伴链接类型( p a r t n e r l i n k t y p e ) 的定义。该类型定义封装了交互的接口关系，即提供服务方 需要定义交互过程中所扮演的角色并给出服务的抽象接口，这是b p e l 抽象与实现剥离特性的 基础。在基于b p e l 的业务流程中，外部的w e b 服务可像黑盒一样来为流程提供所需的服务， 而不需要考虑开发的平台、异构系统等问题。 b p e l 除了用来指定可执行流程，还可以用它来指定抽象流程。抽象流程主要用于定义某 一个伙伴为了达到业务目的和它的其他伙伴交换的消息和可能的顺序。它可被看作可执行业 务流程的外部视图，省略了部分内部执行细节和复杂性。一般来说，抽象流程可以用来呈现 可执行流程的某些方面，通过抽象手段使得人们易于理解和沟通：或者以简单的抽象流程作 为设计流程的起点，通过不断精化和改进，构建出复杂的可执行流程。抽象流程还可以用来 实现协议匹配，来判断两个业务伙伴是否能够互相交互。 b p e l 使组织能够通过编排服务来自动化他们的业务流程。它强迫组织围绕服务来设计将 来的业务执行流程，例如将现有功能公开为服务、使用服务构成新的应用程序、在不同的应 用程序中重用服务等等。 2 1 1b p e l 的作用域 b p e l 语言编写的程序支持两类任务或者行为：基本任务( b a s i ct a s k s ) 和结构化任务 ( s t r u c t u r e dt a s k s ) 。基本任务是指由业务流程的一个基本的步骤，任务内不会嵌套其它任 务：而结构化任务是至少包含一个基本任务的业务流程。 基本任务包括： i n v o k e 任务一一允许业务流程在某一个w e b 服务提供的p o r t t y p e 上调用单向的 ( o n e - w a y ) 或请求响应( r e q u e s t r e s p o s e ) 操作。 r e c e i v e 任务允许业务流程停下来等待消息到来。 r e p l y 任务一允许业务流程对收到的消息发送一个回复消息。 w a i t 任务通知流程等待一段时间。 a s s i g n 任务一把数据从一处复制到另一处。 t h r o w 任务一表明发生了某个错误。 t e r m i n a t e 任务一终止整个编排实例。 结构化任务包括： s e q u e n c e 任务一定义一个有序的任务序列 s w i t c h 任务根据条件选择某一分支 p i c k 任务停下并等待某一适当消息的到来，或者等到超时继续前进。只要多个触发 器中的一个发生，就执行相应的活动，任务便结束了。 w h i l e 任务一定义循环执行，直至满足某一个条件的一组任务。 f l o w 任务一表明一组应并行执行的步骤( 可以通过建立连接来定义一个特定流程的执 行序列) 以上是是b p e l 4 w s l 1 中常见的任务，在最新发布的w s - b p e l 2 o 有较大的改变。支持更 多新的任务或行为( i f - t h e n - e l s e ，r e p e a t u n t i l ，v a l i d a t e 。f o r e a c h ，e x t e n s i o n a c t i v i t y ) b p e l 用变量表示流程中交换的特定数据。b p e l 流程在收到一个消息后，会为相应的变 8 两南大学硕士学位论文第2 章基本理论 量赋值，以便后续请求能够访问。b p e l 支持的变量类型包括三种： 1 由w s d l 文件所定义的消息类型( m e s s a g et y p e ) ： 2 由x 姐，s c h e m a 所定义的简单类型( s i m p l et y p e ) ： 3 由x 池s c h e m a 所定义的元素( e l e m e n t ) 每一个变量都在一定的所属范围内有定义，超出此范围变量变得无效。为了表示这种范 围，b p e l 用作用域( s c o p e ) 来表示流程中的一个区域。如前所述，某个作用域内的变量只在 该作用域内有效，但b p e l 还扩展了作用域的功能，具体体现在如下几个方面： 1 )错误处理( f a u l th a n d l e r ) 当一个行为出错的时候，会抛出一个错误消息。该消息首先会被自身的错误处理器( 如果 有的话) 所处理。 2 )事件处理( e v e n th a n d l e r ) b p e l 中定义了两类事件：一类是“消息事件”，即从外部传来的消息：另一类是由于达 到了用户定义的时间点而发出的警告。事件处理机制从作用域的一开始就激活，一直等待事 件的到来而执行内部行为，也会随着作用域的结束而结束。 3 ) 补偿服务( c o m p e n s a t i o nh a n d l e r ) 补偿处理是为了将流程的状态回滚，回到跟进入作用域前一样。所需要做的就是将该作 用域内已执行部分采用其它行为进行撤销，通常是调用一个效果相反的服务。 错误及补偿处理程序与o o p 语言( 如j a v a ) 中的c a t c h 子句类似。如果执行了某个抛出 任务，就会触发错误及补偿处理程序。 2 1 2b p e l 的补偿处理 大多数企业都拥有一个迥然不同的应用程序基础架构，其中包含由多个供应商提供的、 在不同平台上运行以及使用完全不同的技术创建的各种应用程序。为了解决这些集成难题， t i b c o 、w e b m e t h o d s 、v i t r i a 以及s e e b e y o n d a 等公司在过去的十年里相继推出了传统的企 业应用程序集成( e a i ) 产品。在过去的几年里，许多企业在这些e a i 解决方案上进行了大 量的投资。因此，e a i 领域中的业务集成通常锁定到单个供应商，并且集成组件被紧密耦合 在一起。 b p e l 的好处在于提供了一个基于标准、与平台无关的解决方案。从而解决了所有这些问 题。松散耦合的b p e l 流程消除了供应商锁定、降低了集成成本并提供了互操作性；此外， 它还增加了一个完善的安全性、异常管理和日志记录层。最重要的是，公司可以利用他们的 现有可能异构的基础架构，使它们充分发挥效用，并使用b p e l 对其进行编排。 一个优秀的业务流程实施都离不开精心设计的错误管理、安全性和记录框架，b p e l 作用 域和补偿处理程序就在这方面增强了流程的强健性和容错性，以及保护了b p e l 流程和相关的 服务。b p e l 使用块状结构，在定义局部环境时可以定义适用于这个环境范围内的变量。此外 故障处理、补偿处理和事故处理也可以与局部环境相连。 事务对于业务交互来说至关重要，为了保证一致性，一个a c i d 事务用到的数据库条目通 常会在处理过程中被锁定。如果事务失败，数据库将会回退到之前的状态。这一功能由数据 库提供商提供。对于一组被调用的w e b 服务，b p e l 也可以采用类似的思路，使用w e b 服务的 9 两南