一种Web服务组合一致性验证方法研究

马薇薇　王进　姜家鑫

摘要：为解决Web服务组合事务放松ACID属性后，原子性与一致性无法保证同时满足的问题，提出了一种基于有限状态自动机的服务组合概念一致性检测方法。与以往大多通过运行时监控和协调保证应用一致性的方法不同，该方法采用有限状态自动机在设计阶段对服务组合的交互行为与异常处理进行建模，分析了概念一致性满足的关键条件和性质，证明了服务组合概念一致性的判定定理。最后通过分析服务组合一致性检测的实施框架说明了该方法的可行性。

关键词：Web服务组合；确定有限状态自动机；事务；一致性检测

中图分类号：TP311文献标识码：A

Abstract：To solve the problem that atomicity and consistency cannot be guaranteed to satisfy at the same time when ACID properties are relaxed in Web services composition transaction.A Deterministic Finite State Automata（DFA） based approach is presented to check the conceptual consistency in services composition.Different from most previous works which keep application consistency by runtime monitoring and coordination，this approach uses DFA to model interaction behavior and exception handling process of services composition at design stage.The DFA based approach analyzes the key conditions and properties to satisfy the conceptual consistency；and further，it proofs the theorem to determine the conceptual consistency in service composition.Finally，by analyzing the deployment framework of services composition consistency detection，the feasibility of our approach has been illustrated.

Key words：Web services；DFA；transaction；consistency checking

1引言

面向服務计算模式（SoC）以可重用服务为构造单元，为解决分布式应用集成提供了新型计算范型[1，2]。服务作为自治、自描述和平台独立的模块化应用[3]。为企业间协作提供了协作基础。但单个服务本身功能单一，无法提供完整解决方案。因此，必须对服务进行组合和协作以实现复杂B2B业务逻辑[4，5]。Web服务资源自治性高，潜在故障多，可长期运行等特点引发了Web服务组合协作的一系列新需求（如死锁处理，兼容性检测等）。这其中，保持服务组合后应用一致性是一个关键问题[6，7]。在Web服务组合中引入事务概念，利用事务“非全则无”的语义可以有效增强服务组合的可靠性，保障参与组合数据与应用自身状态的一致。但Web服务由于其运行长周期，异构等特点，不可能按照传统事务严格锁定的方式来管理资源。对传统事务的ACID属性进行适当放松成为必然。

在Web 服务组合事务模型中，主要通过异常处理这样一种相对柔性的方式来达到概念上的原子性与一致性[8，9]。文献[10]提出的Saga模型是最早应用于Web事务领域的事务模型之一。Saga模型将一个完整事务分解为若干个子事务，并为每个子事务设计业务逻辑上相对应的补偿事务，在失效情况下，执行失效部分的补偿事务以达到语义上的一致性与原子性。文献[11]提出的全局事务模型对Saga模型进行进一步扩展，提出全局回滚以及局部回滚的概念来处理不同失效场景。在Saga模型与全局事务模型中，都严格要求对失效的操作进行补偿。实际应用场景中，往往对于某些子事务操作由于补偿代价过高而无法真正进行补偿。文献[12]针对单一补偿方式的不足，提出了后向补偿与前向的替换（重试）相结合的异常处理方式，这一处理方式在目前服务组合事务处理相关研究中被广泛采纳。

文献[13]在文献[12]的基础上，通过定义服务组合原子范围（atomicity sphere）实现业务流程放松的原子性要求。在此种半原子性模型中，每个子事务都具备可补偿性与可重试性这两个正交属性。该模型可在参与业务流程的服务未隐藏业务细节时，检查流程的原子范围，构建可靠的组合服务。文献[14]使用进程代数对服务组合进行了建模，并通过引入公理系统的方式，检测组合的原子范围。但其公理系统主要是为顺序和选择结构提供规约，对并发情况下的交错时序考虑较少。文献[13，14]中所采用的半原子性模型，不能保证组合事务在符合放松的原子性时同时满足一致性。文献[15]针对以上的事务模型进一步提出了面对长周期事务的调度算法和层次式失效恢复算法.这些研究主要集中于在运行期间通过协调和调度保证最终结果的一致性，对设计阶段一致性检测少有涉及。文献[16]提出集合一致性（set consistency）的概念来检测设计时的一致性，但该方法需要用户定义一致性满足条件。这种一致性条件更多反映的是业务需求上的一种约束，对事务概念层上的一致性难以描述。

针对以上研究中的不足，本文试图给出一种针对原子范围理论原子性定义下的服务组合建模方法。endprint

本文首先结合案例分析了服务组合一致性检测问题的产生，对服务组合的交互行为及其异常行为进行基于确定有限状态自动机的建模。针对建立的异常行为模型，提出并证明了概念一致性的判定定理。并且考虑到服务组合异常模型可能产生的状态爆炸问题，进一步提出了对异常行为模型的约简方法。

2服务组合一致性问题及其建模

21Web服务组合一致性问题描述

与传统严格锁定的事务ACID属性必然同时满足不同，在异常处理方式中，事务满足原子范围并不能保证其同时满足一致性要求。根据事务自身一致性的定义可知，服务组合事务满足事务概念上的一致性应保证任意事务执行路径上的子事务出现异常时，通过异常处理及后续一系列补偿或重试操作，最终可以到达初始或者终止状态，且不会存在多条可能的事务执行路径最终所到达的终止状态间存在冲突。

考虑图1所示的“秒杀购物”场景。该服务组合包括填写订单（Fill_Order）、支付（Make_Payment）、预订（PreOrder）、查找商品（Check_Item）、发货（Ship_Order）这五个子事务，事务要求保证同一用户仅能秒杀一次。在该组合流程中，用户首先填写订单，接着进入一个并发的流程，用户可以进一步立刻支付或选择预订，商家同时进行查找商品和发货操作，当用户和商家操作并行完成后，此订单处理结束。这五个子事务中，支付服务由于其需要和外部支付代理交互，因此为不可补偿也不可重试 （NC，NR），根据原子范围定义，这一支付服务为关键（Pivot）子事务。发货服务往往由于其成本原因一旦执行就不可补偿，因此其事务属性为不可补偿但可重试（NC，R），预订服务由于秒杀购物的特殊性，一旦出现异常则只能补偿，不可重试（C，NR），而其余参与服务的子事务都假设其事务属性为可补偿可重试（C，R）。在此服务组合中，存在3条可能的并发路径：

①Fill_Order->Make_Payment

②Fill_Order->Pre-Order

③Fill_Order->Check_Item->Ship_Order

单纯考虑此3条路径，都满足原子范围中所定义的原子性。但若考虑并发流程时序上可能存在的交错性，对并发行为进行组合后，在全局序列上将可能存Fill_Order->Check_Item->Ship_Order->Pre-Order，在此序列中Ship_Order这一仅可重试的服务在Pre-Order这一仅可进行补偿的服务前发生，从而将导致原子范围的违背和应用不一致的发生。

另一方面，考虑两操作者A，B以同一用户ID在异地同步执行此服务组合。若A执行的最终流程为Fill_Order->Make_Payment->Check_Item->Ship_Order，B最终执行的流程为Fill_Order->Pre-Order ->Check_Item->Ship_Order。由于A执行流程中包括一个关键子事务Make_Payment而B不包括，则最终将导致出现同一用户购买了两次，或者系统中对用户是否支付的状态上出现不一致的状况。

从以上分析可知，在设计阶段检测服务组合事务一致性时，除考虑原子性的满足外，还必须考虑其并发状况下的时序组合及关键子事务所处位置。

22基于确定有限自动机的Web服务组合建模

定义2.1Web服務组合的确定有限状态自动机（DFA）模型。Web服务组合的确定有限状态自动机模型可定义为一个五元组A=（Q，Σ，δ，q0，F）。其中，Q 是一个有限的状态集合；ΣM表示请求一个组合中服务消息的有限集合，其中M为服务组合中的服务消息集合；δ：Q×∑→Q表示自动机中的所有变迁；q0∈Q表示初始状态；FQ代表终止状态的集合。

定义2.1中的模型是所有可能消息传递的组合结果，因此定义2.1中的模型事实上包含了当前事务的所有可能执行路径。

文献[17]对服务组合构造自动机模型的过程进行了分析，本文首先利用上述文献中的方法构建一个仅包含基本的消息传递的有限状态自动机。图2为图1所示场景经过转换所得的确定有限状态自动机。

设定义2.1中服务组合的DFA模型拆分后的自动机为Asplit 。我们将以Asplit作为服务组合一致性研究的基础模型。

定义2.2完全状态迹。对Asplit中的qn∈F，如果，σ1，σ2，...，σk∈∑，使得q0×σ1→q1，q1×σ2→q2，...，qk-1×σk→qn，则称q0，q1，...，qn的序列为Asplit上的一个完全状态迹ω，Asplit上的所有完全状态迹的集合记为Trace（Asplit）。

由完全状态迹定义可知，ω即代表Asplit上的一条事务执行路径。Trace（Asplit）为Asplit中所有可能的事务执行路径集合。考虑到事务一致性判定中需要基于同一事务执行路径同时刻画正常执行与异常执行下的变迁，定义2.2采用状态迁移序列替代了通常由变迁序列所定义的自动机迹。在Asplit中由于任意两个状态间的迁移仅可能由唯一变迁引发，因此状态序列将与变迁序列具备一一对应关系。

图2秒杀购物场景服务组合确定有限自动机模型

定义2.3部分迹。在Asplit在中，对q∈Q，q*代表从状态q出发可能到达的状态集，如果q，q1，...，qn∈q*，σ1，σ2，...，σk∈∑满足q×σ1→q1，q1×σ2→q2，...，qk-1×σk→qn，则称 q，q1，...，qn所组成的序列为q到qn的部分迹，记做μ（q，qn）。

23异常处理模型

由文献[10]可知，每个服务变迁所对应的子事务都有两个正交的属性：可补偿性与可重试性。将两正交属性组合后，可得任一子事务其事务属性取值集合为{（C，R），（C，NR），（NC，R），（NC，NR）}。endprint

定义2.4可补偿变迁集SC。对σ∈∑，如果Comp（σ）=C则qσq′的变迁都属于SC。其中Comp（σ）为获得子事务可补偿属性的函数，其值域为{C，NC}。

定义2.5可重试变迁集SR。对σ∈∑，如果Retry（σ）=R则qσq′的变迁都属于SR。其中Retry（σ）为获得子事务可补偿属性的函数，其值域为{R，NR}。

定义2.6关键变迁集Spivot。对σ∈∑，如果Retry（σ）=NR∧Comp（σ）=NC则qσq′的变迁都属于Spivot。

根据定义2.4-2.6，我们可在Asplit基础上针对子事务的异常行为进行建模。根据2.1节中事务概念一致性分析可知，需要对Asplit进行补偿与重试扩展，扩展规则为：

①对qσq′∈δ∧qσq′∈Sc ，δ=δ∪q′τcq；

②对qσq′∈δ∧qσq′∈Sr，δ=δ∪q′τrq.

因为在Asplit中我们已保证任意两个状态间仅可能由一个变迁引发，所以上述扩展规则将具有唯一性，基于此扩展后的δ可得：

定义2.7支持异常处理的扩展有限状态自动机Aexec。Aexec也为五元组（Q，∑exec，δ，q0，F）：Q，δ，q0，F与定义2.1相同；∑execM∪{τc，τr}，其中M同定義2.1，{τc，τr}为异常行为变迁动作，分别对应补偿动作和重试动作引发的变迁。

对于SC集合中的元素，都为可补偿子事务，其异常处理方式为执行补偿任务并恢复到未执行前的状态。在Aexec中，所有τc补偿动作所引发的变迁集合为补偿变迁集，其形式化的定义为：

定义2.8补偿变迁集TRc。在Aexec中q∈Q，如果qτcq′∈δ，则qτcq′∈δ∈TRc。

类似的，SR集合中的元素，都为可重试子事务，其异常处理方式为不断重试当前动作直到其成功变迁到下一状态。在Aexec中，所有重试动作所引发的变迁集合为重试变迁集，其形式化的定义为：

定义2.9重试变迁集TRr。在Aexec中q∈Q，如果q′τrq∈δ，则q′τrq∈δ∈TRr。

从文献[14，18]对服务组合事务一致性分析可知，组合事务能否保持一致性仅和其异常处理动作相关。事务发生异常时，若整个事务要保持一致性，则必然可通过若干重试变迁到达终止状态，或通过若干补偿变迁到达初始状态。结合定义2.6中的Aexec与TRc，TRr两个变迁集合，可构造出仅包含异常处理相关动作和变迁的确定有限状态自动机。

定义2.10异常处理确定有限状态自动机Aexhandler。Aexhandler为五元组（Qcr，∑cr，δcr，q0，Fcr）：q0同定义2.1；Fcr：F-f∈F∧fτcq′∈TRc∧q′τrf∈TRr；Qcr：Q-q∈Q∧qσq′∈TRr∪TRc∧q′σq∈TRr∪TRc；∑cr∈{τc，τr}；δcr∈TRr∪TRc.

Aexhandler模型，由于仅考虑异常处理相关变迁，其变迁集合为补偿变迁集和重试变迁集的并集，其变迁动作仅能为{τc，τr}中的一个。由Aexhandler构造过程易知，对Asplit中的状态集Q，如果q∈Q其事务属性唯一确定，则Asplit所构造的Aexhandler具备唯一性。

Aexhandler中终止状态集Fcr为Asplit中的终止状态集F去除所有孤立终止状态后所得。某终止状态为孤立终止状态当且仅当此状态所有的前继变迁都为关键子事务。在此情况下，该终止状态将紧随关键子事务发生，进行一致性判定时，仅需考虑关键子事务前所有状态即可，所以将此类孤立终止状态从终止状态集中去除。

Aexhandler中的状态空间Qcr为Asplit状态空间去除所有孤立状态所得。状态为孤立状态当且仅当其所有前继和后续变迁均为关键子事务。此类状态的出现意味着服务组合中出现了不止一个关键子事务，此种情况与事务原子范围的原子性违背，所以对这类状态的去除，同样不影响一致性判定。

3Web服务组合一致性检测

31服务组合一致性判定

定义3.1补偿迹。在Aexhandler中，μ（q，qn）称为q的补偿迹，记做μcomp（q），当且仅当μ（q，qn）所代表状态序列中任意两个相邻状态之间的变迁都为τc。所有μcomp（q）的集合记为Tracecomp（q）。

定义3.2重试迹。在Aexhandler中，μ（q，qk）称为q的补偿迹，记做μretry（q），当且仅当qk∈q*∧qk∈Fcr使μ（q，qk）所代表状态序列中任意两个相邻状态之间的变迁都为τr。所有μretry（q）的集合记为Traceretry（q）。

由于在Asplit中已针对可能存在的并发时序交错建模，对Asplit进行概念一致性判定时，我们仅需考虑如下两个问题：

问题1：是否每个事务执行路径中的任意一个状态出现异常时，事务都能保证放松的原子性；

问题2：整个事务中的关键子事务是否会导致最终事务出现多个不一致的最终状态。

定理1（事务一致性判定定理）。对服务组合系统，若其对应的Asplit可唯一构造异常处理有限状态自动机Aexhandler，服务组合满足事务一致性，当且仅当：

①在Asplit上，σ∈Σ∧qσq′∈ Spivot→（σ1∈∑∧σ≠σ1∧qσ1q′∈Spivot）

②在Asplit上，对σ∈Σ，如果qσq′∈Spivot，则对 ω∈Trace（Asplit） →qi，qj∈ω∧qiσqj∈δ；

③对q∈Qcr，ω∈Trace（Asplit）如果q在ω 所代表的序列上，则在Aexhandler上有：（μ（q，q0）ω→μ（q，q0）∈Tracecomp（q））∨（（qn ∈Fcr∧μ（q，qn）ω）→μ（q，qn）∈）Traceretry（q））.endprint

3.2服務组合一致性判定实施框架

在第2章中，对服务组合及其异常处理进行建模，在本节将讨论服务组合的一致性判定的实施框架。图 3 位服务组合一致性判定的实施框架。

结合第2章的分析，讨论此实施框架的可行性。

Step1：流程的抽取

在此步骤中，服务设计者根据应用规约完成服务组合流程设计。在实际应用场景中，服务组合的建模方式具有多样性（如UML活动图，BPEL，形式化描述等）。但任何一种建模方式，其最终模型都将包含：参与流程的服务、服务间交互行为以及流程的基本结构这三个元素，从而使得根据这些组合模型转变为本文中的有限状态自动机模型成为可能。目前已有大量 Pi 演算、Petri 网、UML 活动图和 BPEL 等流程模型向自动机模型转换的相关研究，因此选取自动机作为服务组合流程的描述，将不会成为实际实施的限制与障碍。

Step2：流程对应的确定有限状态自动机的构建

根据第2章分析易知，在此步骤中需要完成事务状态空间分析，事务初始与终止状态设定，状态之间迁移动作分析并在此基础上完成自动机的构建。这个过程可以由设计人员根据应用规约手动进行，也可以根据第 1 步中的流程建模结果以及原始模型与有限状态自动机模型之间的转换规则进行自动转换得到。通过这样方式构建的有限状态自动机中将往往包含两个状态间存在不同迁移动作的状况，为后续的异常分析能够进行，还需要对此原始自动机进行状态拆分，得到任意状态转变都仅由唯一迁移引发的Asplit模型。

Step3：事务相关属性的获取

事务属性采用文献[10]提出的可重试性与可补偿性概念。对组合事务的每个子事务设定事务属性时需要流程设计人员对全局事务的处理工作具有一定的了解，同时综合考虑补偿代价等因素进行。本文与之前大量服务原子性与一致性相关研究一致，采纳了任意子事务其事务属性唯一确定的假定。但我们也注意到，实际应用环境下，由于应用的复杂性，服务本身可能具备不同状态，同一服务在不同状态下，将有可能具备不同的事务相关属性。如对于银行卡验证服务，当用户验证出错次数小于 3 次时，其可重试性为 R，但当出错次数大于 3 时，其可重试性将为 NR。我们将在后续的研究中针对这一情况开展进一步的分析。

Step4：定理 1 中条件 1，2 的检测

针对定理 1 中的条件 1 和条件 2，需要判断关键子事务出现次数和位置。因此直接在Asplit上进行检测。在实际实施过程中，这一步骤可以和步骤 5 同步进行，我们将在下一节算法分析中对此进行详细的讨论。

Step5：异常处理模型的构造

根据 2.2 节的分析，完成此步骤首先需要根据步骤 3 中事务属性在步骤 2 的结果上附加补偿变迁与重试变迁。

Step6：约简模型上对定理 1 条件 3 的检测，由于篇幅受限，本文并未介绍模型的约简过程。

在约简模型上的检测可以得出一致性的最终判定结果。但我们也注意到，目前的检测方式不方便业务人员快速定位一致性违背出现位置，这也将是我们的未来工作之一。

4结束语

Web服务组合中引入事务概念可以有效保障应用一致性增强服务组合的可靠性，但传统的数据库事务的严格锁定资源的方式不适合长周期、松耦合的服务计算环境。异常处理方式放松了ACID的要求，通过柔性模型达到概念上的原子性与一致性，此时满足放松原子性的事务，不再能保证同时满足事务概念上一致性，需要对服务组合的一致性单独进行检测。

本文基于确定有限状态自动机，对服务组合的交互以及异常处理进行了建模，在此模型上进一步提出了服务组合一致性的判定定理。最后针对整个检测过程，分析了其实施框架及主要步骤。

本文的进一步工作将包括对原始异常处理模型的约简，以及同时兼顾概念一致与应用需求一致性的检测以及在跨机构环境下，基于等价替换与公开视图的组合建模与一致性判定。

参考文献

[1]PAPAZOGLOU M P，GEORGAKOPOULOS D.Service oriented computing[J].Communications of the ACM，2003，46（10）：2428.

[2]MUTANU L，KOTONYA G.ConsumerCentred Validation for Runtime Adaptation in ServiceOriented System[C]// IEEE，Conference on ServiceOriented Computing and Applications.IEEE Computer Society，2016：16-23.

[3]TSALGATIDOU A，PILIOURA T.An overview of standards and related technology in Web services[J].Distributed and Parallel Databases，2002，12（2-3）：135-162.

[4]QIAO X Q，WEI J，HUANG T.Service collaboration approach based on decentralized mediation model[J].Journal of Software，2009，20（6）：1470-1486.

[5]WIETRZYK V I，LAWSON R，TALIZAWA M，et al.Multimedia Distributed Infrastructure for B2B Operations in Web Services.[J].Ultraschall in Med，2016，4（01）：936-942.endprint

[6]GREENFIELD P，KUO D，NEPAL S，et al.Consistency for web services applications[C]//Proceedings of the 31st international conference on Very large data bases.VLDB Endowment，2005：1199-1203.

[7]PAPAZOGLOU M P，TRAVERSO P，DUSTDAR S，et al.Serviceoriented computing：A research roadmap[J].International Journal of Cooperative Information Systems，2008，17（02）：223-255.

[8]CASATI F，CUGOLA G.Error handling in process support systems[M]//Advances in exception handling techniques.Springer Berlin Heidelberg，2001：251-270.

[9]HASHMI K，MALIK Z，NAJMI E，et al.A Web Service Negotiation Management and QoS Dependency Modeling Framework[J].Acm Transactions on Management Information Systems，2016，7（2）：1-33.

[10]GARCIAMOLINA H，SALEM K.“SAGAS，”[J].SIGMOD Record，1987，16（3），249-259.

[11]GREFEN P，VONK J，APERS P.Global transaction support for workflow management systems：from formal specification to practical implementation[J].The VLDB JournalThe International Journal on Very Large Data Bases，2001，10（4）：316-333.

[12]LEEPA，ANDERSON T，Fault Tolerance：Principles and Practice，pp.143-185.SpringerVerlag，1990.

[13]HAGENC，ALONSO G.Exception Handling in Workflow Management Systems[J].IEEE Trans.Software Eng.，2000，26（10），943-958.

[14]YE C，CHEUNG S C，CHAN W K，et al.Atomicity analysis of service composition across organizations[J].IEEE Transactions on Software Engineering，2009，35（1）：2-28.

[15]REN Y，GUAN J，AO Q，et al.LHFR：A hierarchical failure recovery algorithm for long running transactions[J].Journal of Computer Research & Development，2010，47（10）：1805-1811.

[16]FISCHERJ，MAJUMDAR R.Ensuring Consistency in Long Running Transactions[J].Proc.22nd IEEE/ACM Intl Conf.Automated Software Eng.，2007，54-63.

[17]WOMBACHERA，FANKHAUSER P，NEUHOLD E.Transforming BPEL into annotated deterministic_nite state automata for service discovery[C].In Proceedings of the 2nd IEEE International Conference on Web Services，pages 316{323，San Diego，CA，USA，July 2004.IEEE.

[18]SCHULDTH，ALONOSO G，BRRRI C，et al.Atomicity and Isolation for Transactional Processes[C].ACM Trans.Database Systems，2002，27（1），63-116.endprint