Web 服务交互过程建模与验证研究

包 力

（内蒙古工业大学，呼和浩特 010080）

随着现代经济社会全面进入服务经济时代，现代服务业已经成为了现代经济社会持续发展的新动力[1]。Web 服务即用户根据实际的生产需求可弹性获取，由云提供商提供的、可扩展的计算资源。然而，单一Web服务只能提供有限的计算资源。比如，糖尿病患者需要关于如何控制餐后血糖进行信息咨询，这样的信息咨询将在减缓病情发展方面发挥积极作用。影响糖尿病患者餐后血糖的因素有很多，比如胰岛素剂量、每餐热量摄入、日常锻炼等常见因素都可能影响餐后血糖。如果糖尿病患者想预测并干预餐后血糖，就需要这些方面的数据。可用于收集相关数据的常见软件服务有记步服务、热量摄入记录服务、医疗数据分析服务等分属不同的云平台，显然，单一的软件服务无法满足上述需求，需要组合血糖控制咨询服务（负责回答患者问题并提供建议）、记步服务（负责记录患者燃烧的热量）及数据分析服务（负责处理和分析数据）。由这些服务构成的服务组合，将为糖尿病患者提供关于血糖方面的信息咨询。Web 服务组合（以下简称“服务组合”）就是根据客户需求的变化动态增加或释放所需的资源，将跨越不同服务提供商的Web 服务进行整合，为用户提供增值服务并实现更加复杂的功能。服务组合旨在有效选择、整合来自不同云平台的服务，将跨越云平台边界的服务进行深度整合并实现其功能的扩展与创新，使得这些服务协同工作，为用户提供更加全面、更高质量的功能。跨云服务组合技术将为现代服务业的发展注入新动力。

本文组织如下：第1 节介绍相关研究工作，第2 节介绍Web 服务交互模型，第3 节给出Web 服务交互模型的行为语义，第4 节提供了一个案例研究，最后是结论和展望。

1 相关研究

Web 服务组合（Web Service Company）是以业务流程和规则为基础，将若干组件式服务组合成粒度更大的、服务的过程。服务组合方法大体上可分为基于业务流程驱动的服务组合和基于即时任务解决的服务组合两大类。一是基于业务流程驱动的服务组合，二是基于即时任务解决的服务组合。

在面向Web 服务的自动化组合方面有许多研究成果。文献[2]研究了云制造中的服务重构与供需衔接问题，提出了面向云制造的自主性导向（autonomy-oriented）服务组合与优化选择方法。为了提高服务选择的准确性，研究者给出了带有波动率分析功能的、基于模糊集的决策方法。针对利用语义web 服务发现机制发现并选择最合适的候选服务问题，文献[3]给出一种由5 个阶段构成的多级工作流编排框架。该框架采用功能属性描述候选服务的行为，并可满足用户目标的动态变化。文献[4]提出了一种混合Web 服务自动组合方法，旨在生成具有最佳端到端QoS 的基于语义输入输出的服务组合，并使参与组合的服务数量最小化。为了使开发者能够高效地进行服务组合，文献[5]给出了一种可视化的REST 服务建模框架，该框架由可视化服务组合建模工具和服务开发平台组成。为了提高Web 服务组合测试用例的质量并找出哪条路径导致服务组合失败的概率最大，文献[6]采用启发式测试用例生成法以获得最优测试路径。

2 交互Web 服务网络

2.1 Kahn 过程网络

Kahn 过程网络（KPN）[7]是一种基于数据流的计算模型，该模型的优点之一是可以在分布式结构上实现进程的并发通信和执行，这一特点使得KPN 非常适合于建模Web 服务交互行为。在KPN 模型中，并发过程使用节点表示，有序的数据序列使用弧表示（数据序列也称为令牌）。进程通过先进先出的通道相互通信，在KPN 中，使用数据令牌队列表示这些通道。启动FIFO通道的读取操作需要通信通道中至少存在一个令牌。由于FIFO 通道的大小是无限的，因此写入操作是非阻塞的。KPN 模型采用异步通信，并且KPN 计算的输出结果与其执行顺序无关，即进程并发过程中先执行哪个进程对计算结果不产生影响。

2.2 Web 服务交互网络IWSN

在IWSN 模型中，Web 服务被建模为KPN 中的计算进程，Web 服务组合被建模为进程的并发自治网络。进程间通过先进先出的通道进行通信。网络中的每个进程都对消息序列进行自主控制，并且每个进程执行的操作与其他进程的操作并发执行。对于单个进程（服务），其行为建模为其执行的操作。Trace（记录）用于建模进程之间的交互行为，IWSN 模型如图1 所示。

图1 Web 服务交互网络

2.3 交互Web 服务网络的定义

由于操作是Web 服务功能的基本单元，IWSN 中Web 服务调用被建模为操作的调用过程，这里使用集合Operation表示。IWSN 中，使用进程（Process）建模服务顺序执行操作的集合，即Process集合中的一个元素是操作的线性串联。如果一个操作op1的输出消息是另一操作op2的输入消息，那么在op1和op2之间存在对应关系，这里引入二进制关系Ro来表示这种类型的关系。在IWSN 中，符号T用来表示进程（Web 服务）的交互记录。

定义1（交互Web 服务网络）。

一个交互Web 服务网络是一个6-元组，在这里

Service是Web 服务的集合;

Process是进程的集合;

Operation是操作的集合;

T表示操作序列的集合;

Message表示出入进程的消息的集合;

Ro⊆Operation×Operation是Operation集合上的二元关系。

3 交互Web 服务网络的形式化语义

本节给出Web 服务交互网络的行为语义定义，该语义基于Pi-演算及其公理化操作语义[8]。行为语义由2 部分构成，语义转换域和转换函数。首先引入Pi-演算作为语义转换域，然后给出转换函数定义和转换算法，将IWSN 模型语义转换为Pi-演算表达式。

设存在可数无限集N，在Pi-演算中进程（Process）使用N中的元素P，Q，R……（大写字母）表示，进程执行的动作使用N中的元素u，v，w，x，y，z……（小写字母）表示。Pi-演算表达式使用下面的语法构造

式中：使用数字0 表示空进程，空进程已经结束，不执行动作;符号∑表示非确定性选择，例如，R+P表达式表示执行进程R或P中的一个; 进程顺序执行的表达式为cx.P，其中P是进程，c是通道名，x是动作名称，cx.P从通道c读入动作x，然后执行P；表达式P1|…|Pn表示并行执行进程P1，P2，…，Pn；表达式[x=y]P表示当通道名称x与通道名称y相等时，进程[x=y]P的行为与进程P相同，否则[x=y]P为空进程。

4 案例研究

4.1 车辆保养维修服务案例

本节通过汽车保养维修服务案例展示如何应用IWSN 模型建模和验证Web 服务组合的案例，因为重点建模的服务交互行为，所以服务组合涉及的其他方面的技术细节没有建模。通过这个案例可以看出，即使相对简单的服务组合也会包含复杂的交互行为。

业务流程简介如下：汽车保养维修服务（Car Maintenance Providing Service）接受客户服务（Client Service）的请求，并根据汽车零部件供应商服务（Vehicle Parts Providing Service）和在线金融服务（On-line Financial Service）的响应，检查该请求是否能够得到满足。在这2个服务确认后，其向客户服务发送一个付款请求。在客户支付了汽车维护费用后，然后将确认消息发送回客户代理。部分消息的含义解释介绍见表1（在每个含义解释的末尾为每条消息定义了缩写）。

表1 部分服务消息含义

下面是基于Pi-演算的单个Web 服务的行为及服务交互的描述（表达式中的! 符号表示发出消息）。

客户服务Client 的行为描述：

Client = ! Request.Interactionloop1

Interactionloop1 = AskInfo.! Pro.Interactionloop1+（Refusal.Client + Accept.! Con.Client）

汽车保养维修服务的行为描述：

当加载到3%rad(38.19 mm)循环时，在位移较大时，角钢微微被掀起。当加载到4%rad(50.92 mm)循环期间，接近位移极值时，角钢被拉起但角钢和梁翼缘为见明显变形。

Car = Request.Interactionloop2

Interactionloop2 = ! AskInfo.ProvInfo.Interactionloop2 + ! GetPartInfo.PartInfo.Interactionloop2 + !GetPaymentInfo. PaymentInfo

Interactionloop2 +τ.（! Refusal.Tour + ! Accept.Con.Tour）

以下表达式分别是车辆零部件供应商服务和在线金融服务的行为描述：

Vehicle = GetPartInfo. ! PartInfo.Vehicle

Financial=GetPaymentInfo.! PaymentInfo.Financial

汽车保养维修组合服务的行为描述：

其中，消息集合{GetPartInfo，PartInfo，GetPaymentInfo，PaymentInfo } 是一组内部消息，需要使用符号τ 来表示发送和接收操作。

4.2 车辆保养维修服务的形式化验证

为了验证服务兼容性，首先需要给出观察等价（Observational Equivalence）的定义。观察等价的定义是判定2 个服务是否兼容的数学基础，同时，观察等价也可用于验证一个服务是否可以替代另一个服务。

定义2 弱迁移（Weak Transitions）。

如果q=q0→τq1→τ…→τqn，那么q⇒εq’，当n≥0，其中，τ 外部不可见动作的迁移标签；

如果q⇒εq’，那么q⇒τq’；

如果q⇒εq1→aq2⇒εq’，那么q⇒aq’（a≠τ）；

如果q⇒aq’，那么从q到q’是一个弱迁移。

定义3 观察等价（Observational Equivalence）。

令R⊆Q×Q，那么当关系R是一个弱等价，如果任何时候t1Rt2都存在如下迁移关系：

如果t1→at1’，即意味着存在某个t2’并且t2⇒at2’，从而t1’Rt2’；

如果t2→at2’，即意味着存在某个t1’并且t1⇒at1’，从而t1’Rt2’；

如果在迁移t1和t2上存在一个弱等价关系，即t1Rt2，那么t1和t2是观察等价关系，或弱等价关系。

定义4 行为兼容（Behavior Compatibility）。

2 个服务p和q是行为兼容的，记作compatible（p，q），如果服务p与q观察等价。

根据这个定义，当服务发生交互时，外部观察者不可能区分2 个过程p和q，并且2 个服务p和q行为兼容意味着其存在相反的行为记录。在本案例中，虽然客户端服务也被认为是一个进程，但是客户端进程不包括在Web 服务组合中。系统的设计目标是按照业务流程生成需求规格，也就是开发的系统需要满足客户的要求，即需要验证车辆保养维修服务是否满足需求规格。因此，服务组合应该与客户端服务在行为上观察等价。客户服务和车辆维修保养服务应该有相反的行为。客户端服务的相反行为是

消息集合{GetPart Info，PartInfo，GetPayment Info，Payment Info} 中定义的是外部不可见的内部操作。此时，忽略ServiceSystem中的内部操作。将得到了一个系统（这里使用表示），该系统与Reverse－Client观察等价。

这里对汽车保养维修服务进行可达性分析，通过可达性分析，可能会发现不正确的系统设计，如死锁和关键功能不能满足需求。使用分支时间逻辑计算树逻辑（Computation Tree Logic，CTL）[9]来验证软件系统是否具有预期属性。首先定义一个逻辑公式来描述系统永远不应该达到的状态，并使用should_receive来表示这种状态。对该状态的解释如下。

如果在有限数量（可能为0）的内部执行步骤之后，在客户服务发送请求消息（Req）后，服务客户一定会从汽车保养维修服务接收到响应消息，则系统的should _receive值为true，使用CTL 描述的系统属性

5 结论与展望

本文提出了一种基于Kahn 过程网络的交互Web服务模型（IWSN），旨在解决Web 服务正确的交互问题，同时保证Web 服务交互过程中的行为兼容性。在介绍Pi-演算定义的基础上，给出了IWSN 模型的形式化语义，并给出了IWSN 模型语义转换算法。在车辆保养维修服务案例中，应用IWSN 模型描述了业务流程，并给出了服务行为兼容的定义。案例的实验结果证明了提出的方法是可行和适用的。

综上所述，基于KPN 的交互Web 服务网络具有并发通信机制、可组合性、可执行性等特点，适合于对Web 服务组合过程中的服务交互进行建模。我们未来的工作是实现Web 服务交互网络的原型系统，为相关技术的市场推广奠定基础。