时间约束条件下Web 服务组合的形式化分析与验证＊

陈志辉 ，吴敏敏

(莆田学院 信息工程学院，福建 莆田351100)

在分布式计算和电子商务中，面向服务计算(Service-Oriented Computing，SOC)已成为一个典型的应用范例［1］，它将可用的服务通过组合的方式来快速构建复杂的应用。Web 服务应用就是采用SOC 的思想:首先，可用的服务是基于标准的Web 服务定义语言(Web Services Description Language ，WSDL)来描述;然后，通过服务组合语言(如BPEL，WSCI 和OWL-S)来实现功能更复杂的服务，称为复合服务［2］。

虽然服务组合语言可描述Web 服务之间的交互行为，但缺少形式化方法来验证Web 服务的行为属性。为此，研究人员已提出一些形式化验证方法。例如，Mohsen R 提出了一种基于事件驱动的方法来验证Web 服务组合［3］，采用BPEL 流程来定义Web 服务组合，而事件演算(EC)用于刻画服务的行为属性。除了事件演算，还有其他形式化的方法，如有限状态机(FSM)［4］、Petri 网［5］、进程代数［6］、类型系统［7］等。

然而，Web 服务组合的正确性检查也包括非功能性需求，如响应时间、性能等。在电子商务应用当中，许多业务场景都有实时性要求，即在一定的时间约束条件下，系统必须完成相应的任务。例如，银行的电子转账无法准时到达对方账户，这可能给商家带来巨大的经济损失［8］。

为此，本文将描述如何使用模型检查技术以验证Web 服务的时间行为属性。在Web 服务技术领域，服务之间的调用是通过消息的方式，即发送和接收消息。一方面，执行操作调用需耗费一定的时间。另一方面，传递消息也需要一段时间。例如，由于通信网络中断，客户端就会无期限地等待服务响应。这种情况下，应该设置服务响应的时间约束。因而，本文扩展了标准的WSDL，增加了时间约束语句来描述Web 服务接口，一个时间自动机用于刻画单个服务接口的时间行为，服务组合可看作是由这些时间自动机所组成的网络，并通过模型检查工具UPPAAL 来自动验证时间的行为属性。

1 案例研究

文中借助提出的一个股票分析案例作为应用场景展开分析，并给出具体建模过程与验证。该应用主要涉及四个服务:股票代理服务(SBS)看作是一个经纪人，他为投资者提供股票投资评估服务;实现SBS 是一个服务组合过程，它与股票研究服务(SRS)和投资管理服务(IMS)之间进行交互;SRS 是由不同的证券公司所提供的服务，包括数据库维护、股票前景预测、股票配置等;IMS 维护投资者相关个人信息数据库;用户交互服务(UIS)提供访问接口功能。通常的流程是，SBS 接收到从UIS发送过来的股票分析请求，经过IMS 验证投资者的个人信息，通过SRS 确认股票投资的可行性。最后，SBS 给投资者提供了一份关于股票投资的可行性研究报告。

除了上述功能需求部分，服务组合的执行过程中必须满足的时间约束。在一些实时性要求高的业务领域(如股市)可能包含下列的时间约束条件:(1)在投资者决定访问SBS 后，UIS 应该在10个时间单位内将请求发送到SBS;(2)在IMS 接收到由SBS 发送过来的请求后，验证投资者的身份信息不超过8 个时间单位;(3)SRS 向SBS 提供投资可行性研究报告时，必须在20 个时间单位内完成。

服务组合过程中也要满足上述的时间约束。例如，如果投资者无法在规定的时间内获得股票投资研究报告，那么整个过程就会失去它的商业价值。此外，还存在这样的情况，即时间约束和服务组合不一致。在上述场景中，各个服务之间的通信时间也应考虑。例如，UIS 应在10 个时间单位内发送一个请求到SBS。但是，由于网络中断，该请求就无法到达它的目的地。

为了验证服务的时间属性，首先需对Web 服务建模时间行为。在接下来，文中将扩展Web 服务接口的时间约束规范，采用时间自动机来建模Web 服务的时间行为，并使用模型检查技术来自动验证服务的时间属性。

2 Web 服务

Web 服务是一个自描述的和独立的软件实体，它利用标准的语言和协议在互联网上进行发布、发现和调用［9］。其中一个关键技术就是Web服务描述语言WSDL，将服务看作为一个抽象的端口集合。WSDL 还定义了Web 服务以何种动作来传送数据。一个动作就是一个操作，数据由消息来表示。相关操作的集合称为一个端口类型。端口类型就是Web 服务所提供的操作集合。例如，一个Web 服务的WSDL 接口定义如下:

＜definitions…＞

＜portType name ="investorAuthentication" ＞

＜operation name="getAuthenti

cation" ＞

＜inputname ="getAuthentica

tionRequest"/ ＞

＜outputname ="getAuthenti

cationResponse”/)

＜/operation ＞

＜/portType ＞

＜message name="getAuthenticationRequest" ＞

＜partname="InvestorID" type="xs:string"/ ＞

＜/message ＞

＜message name="getAuthenticationRequest" ＞

＜partname="InvestorID" type="xs:string"/ ＞

＜constraint transmissionTime ＜=5/ ＞

＜/message ＞

＜message name="getAuthenticationResponse" ＞

＜partname="value”type="xs:boolean"/ ＞

＜/message ＞

＜/definitions ＞

为了描述时间约束，本文扩展了标准的WSDL的constraint 元素。该元素是刻画operation 和message 元素中的时间约束关系，并且是可选的。如果一个操作operation 有时间约束，那么duration 用于规范从接收一个input message 到发送一个output message 的时间单元值。

＜operation name="getAuthenti

cation" ＞

＜inputname ="getAuthentica

tionRequest"/ ＞

＜outputname ="getAuthenti

cationResponse”/)

＜constraint duration=10/)

＜/operation ＞

上面例子的第4 行中，duration 定义了从接收“getAuthenticationRequest”到发送“getAuthenticationResponse”消息必须在10 个时间单元之内。如果在一个message 有时间约束，那么transmission-Time 用于规范该消息message 必须发送到目标的时间单元值。

＜message name="getAuthentication" ＞

＜partname="InvestorID" type="xs:string"/ ＞

＜constraint transmissionTime ＜=5/ ＞

＜/message ＞

在上面例子的第3 行中，transmissionTime 定义了传送“getAuthenticationRequest”的时间不超过5个时间单位。

2.1 Web 服务的形式化模型

一般地，Web 服务模型是由其外部可观察到行为组成的，它通过服务端口来发送或接收消息，以此方式与外部环境进行通信。为了建模这些端口的通信行为，本文引入了在FOCUS 框架中消息流的概念［10］。消息流是一个有限的或无限的消息而组成的序列。考虑到Web 服务的时间行为，将时间帧加入消息流中，则称为时间消息流，其定义如下:

(2)为了实现高密度，采用了靶丸注入和分子束、中性束注入。而靶丸注入和超声分子束注入会降低温度，入射深度也有问题。

定义1(时间消息流) 给定的一组消息M，一个时间消息流＜t，ms ＞是由时间帧t 和一个消息序列ms ∈M*组成的，其中M*是一个有限消息序列组成的集合。

时间消息流是表示在一个特定的时间帧内，Web 服务与环境之间的通信行为。在本文中，时间帧是由一个离散时间的符号来表示，即自然数N。

Web 服务接口是由端口来描述的，如图1 所示，服务通过这些端口与环境进行通信。端口是有方向性的(例如:输入或输出端口)和类型的(例如:端口类型规范了什么样的信息可以由这个端口发送或接收)。

图1 Web 服务与环境进行通信的模型

定义2(接口) 一个接口〈I，O〉是由输入端口集合I 和输出端口集合O 组成的，并且I ∩O = φ;每个端口〈p，MP〉∈I ∪O 包括一个端口的标识符(或名称)和一组消息MP⊆M，这些消息可以通过该端口发送和接收。

定义3(接口类型) 给定一个服务接口〈I，O〉，输入端口集I(输出端口集O)的类型表示为TI=Type(I)(或TO= Type(O))，那么它的类型是一个函数类型:TI→TO。

消息流的概念可用来定义端口历史，一个端口历史是由在该端口上通信的消息而产生的。

定义4(端口历史) 给定一个端口集合P，一个端口历史可看作是从每个端口标识符p ∈P 到消息流〈tp，msp〉的一个映射。^P 表示P 中所有端口历史的集合。定义5(执行) 给定一个接口〈I，O〉，服务的执行e ∈(^I ∪^O)，是属于在该接口下某一个端口历史。

定义6(行为) 给定一个接口〈I，O〉，服务的行为B ⊆(^I ∪^O)，是属于在该接口下的某一个端口历史集合。

由于一个服务行为可看作是输入和输出端口历史之间的关系，则将它定义为一个函数B:^I →δ(^O)。

从概念上，两个服务之间进行通信可看作是一种服务组合方式，而且组合之后的这两个服务就成为了一个服务，称为复合服务。因而，服务组合可定义如下:

定义8(服务组合) 服务S1 和S2 接口分别为〈I1，O2〉和〈I2，O2〉，组合s1 ⊕s2 定义在消息流上，它的接口是〈I，O〉= 〈(I1∪I2)(O1∪O2)，O1∪O2〉，行为是Bs1⊕s2= (B ∈^I →δ(^O)|B⇑〈I1，O1〉⊆Bs1∧B⇑〈I2，O2〉⊆Bs2);其中，B⇑〈I1，O1〉表示行为B 只能约束在〈I1，O1〉中是可观察的。

2.2 时间约束的Web 服务接口

为了描述Web 服务接口的时间约束，本文扩展了标准的WSDL，增加了时间约束标签。C(I，O)表示Web 服务接口〈I，O〉上的一个时间约束，要求该服务的行为应该满足C(I，O)，记作:B | =C(I，O)。

例如，存在一个Web 服务有两个端口:一个输入端口p1 和一个输出端口p2 ，它的接口为〈Is，Os〉以及时间约束C(Is，Os)= 5 。假设

如果| tp2- tp1|≤C(IS，OS)，那么Bs| =C(Is，Os)。

相应地，给定的两个服务s1 和s2，以及时序约束C1(I1，O1)和C2(I2，O2)，s1 ⊕s2 的行为必须满足所有的时间约束，记为Bs1⊕s2| = C1(I1，O1)∧C2(I2，O2)。为了确认该服务组合是否满足时序约束的需求，接下来将先建模每个服务的时间行为，再通过模型检查技术来验证服务组合的时间属性。

3 时间自动机

时间自动机之间通过共享信道进行同步，但不能支持传值通信。为此，可以通过共享变量的方式来实现同步传值通信，首先由输出方给一个共享变量赋值，之后输入方再直接访问该共享变量，获得数值。时间自动机是一种用于描述、分析实时系统行为的形式化模型［11］。它是在传统的有限状态机的基础上增加了时钟变量和时钟约束，用于刻画连续变化的时间。时间自动机的语义被定义为一个标记迁移系统［12］。

给定一个时钟集合X，D(X)为定义在X 上的时钟约束集合，其语法定义如下:

其中，x ∈X，c ∈N，r ∈{＜，≤，=，＞，≥}。定义9(时间自动机) 一个时间自动机可以用一个八元组(S，S0，F，I，O，X，E，Inv)来表示，其中:

(1)S 是一个有限状态集;

(2)S0∈S 是初始状态;

(3)F ⊆S 是一个结束状态集;

(4)I 是一个输入端口集(或输入动作集);

(5)O 是一个输出端口集(或输出操作集);

(6)X 是时钟变量的集合

(7)E ⊆S × (I ∪O ∪{τ})× D(X)×2X×S 是有向边的集合

(8)Inv:S →D(X)是一个映射，为S 中的每一个状态指定D(X)中的某一个约束。

在服务交互过程中，一个状态迁移＜s，a，g，r，s' ＞∈E 可写为，它表示在保证时间约束条件g 为真的条件下，状态s 迁移到s' ，执行了通信动作a ∈I ∪O 或内部动作τ，并重设时钟变量r 为0。时钟赋值是通过一个函数f:X →R+，表示将时钟集合X 映射为非负实数;Rc表示时钟赋值的集合;f ∈Inv(s)表示f 满足Inv(s)约束。

定义10(时间自动机的语义) (L，lo，F，I，O，X，E，Inv)的语义定义为一个标记迁移系统(S，So，→)，其中，S ⊆L ×Rc是一个格局，→⊆S ×(I ∪O ∪{τ}∪Rc)× S 是一个迁移关系，表示如下:

上述迁移关系定义了两种情况:

(1)系统仍处于相同状态但时间发生了推移;

(2)系统立即迁移到另一个状态并执行了一个动作［13］。

多个并发的时间自动机TA1，…，TAn 可构成一个时间自动机网络 TBAN = (X，TA1‖…‖TAn)，该网络中的多个自动机之间通过共享时钟变量X 进行同步。

定义11(时间迁移系统)。假设一个时间自动机网络(X，TA1‖…‖TAn)是由n 个并发的时间自动机TA1，…，TAn，组成的。它的时间迁移系统被表示为一个三元组(Δ，ρ0，→)，其中，Δ ⊆(S1× …× Sn)× Rc是一个状态集合，ρ0=)是一个初始状态，→⊆Δ ×(I ∪O ∪{τ}∪Rc)× Δ 是一个迁移关系，表示如下:

上述迁移关系定义了三种情况:(1)系统仍处于相同状态但时间发生了推移;(2)系统迁移到另一个状态并执行了一个内部动作;(3)系统迁移到另一个状态，并且两个时间自动机之间执行了一个同步动作。

时间自动机上的动作集合对应着Web 服务接口上的端口集合，输入端口p 对应输入动作p?，而输出端口r 对应着输出动作r!。对于同一类型的端口p，如果存在动作p?和p!，那么(p?，p!)表示这两个动作可进行同步通信。

对于Web 服务接口的时间约束，主要关注两个方面:调用操作(通过一个端口接收或发送消息)和传送消息的时间约束。

例如，一个调用操作的时间相关行为，即先在时间点t1接收一条消息m1，然后在t2时刻发送另一条消息m2，该行为可建模为图2 中所示。

图2 调用操作的时间相关行为模型

如果上述调用操作的时间约束要求不超过10个时间单位，则在该时间约束下的行为可建模如在图3 中所示。

图3 时间约束下的调用操作的时间相关行为模型

当Web 服务s1向s2发送消息时，也就是s1在时间点t1发送消息m，然后s2在t2时刻接收该消息，这种行为可被建模为图4 所示。

图4 发送消息下的时间相关行为模型

如果发送消息的时间约束是要求不超过5 个时间单位，那么该行为可建模如在图5 所示。

图5 时间约束下的发送消息时间相关行为模型

4 基于UPPAAL 的模拟和验证

为了模拟服务组合中的时间行为，本文先将Web 服务接口转化为时间自动机，然后利用模型检测工具UPPAAL 来模拟和验证时间自动机网络的时间属性［13］。股票分析应用场景中，主要涉及了四个Web 服务:UIS，IMS，SRS 和SBS，将这些服务和各自的时间约束分别转换为时间自动机，如图6 所示。

图6 服务UIS，SRS，IMS 和SBS 的时间自动机模型

另外，服务的时间属性采用UPPAAL 中的时序逻辑公式来表达。这些公式是建立在计算树逻辑(CTL)的一个子集上，它是由状态和路径公式组成的。状态公式用于描述单个状态的逻辑性质，例如，不变量式t ＜=3;路径公式用于量化模型的路径，其语法表示如下:

这些时序逻辑公式用来刻画服务的具体时间属性，包括:

(1)服务组合的安全性，即复合服务不出现死锁，该属性的时序逻辑公式:

(2)在UIS 发送一个请求之后，它可能从SBS中获得的股票投资研究报告:

E［］ UIS.send Re quest imply SBS.perpare Re port

(3)从UIS 发送请求到SBS 所耗费的时间是不超过10 个时间单位:

A［］ SBS.obtain Re quest imply x ＜= 10

(4)SBS 必须在8 个时间单位内获得投资者身份的确认结果:

A［］ SBS.authentication Re sult imply y ＜= 8

(5)SBS 必须在20 个时间单位内获得研究报告:

A［］ SBS.research Re sult imply z ＜= 20

经过模型检测工具UPPAAL(4.0.13 版本)的自动验证，上述时间属性都满足，分析结果见图7。

图7 股票分析应用场景服务的属性验证结果

5 相关工作

近几年来，已有一些研究者关注对Web 服务组合如何进行建模和分析。为确保Web 服务组合的正确性，Howard 提出了一种基于BPEL 的形式化语义，将其转化成有限状态进程(FSP)模型，并使用LTSA-WS 模型检查工具对服务组合的行为属性进行验证［14］。

Raman 提出了一种基于BPEL 流程定义的Web 服务组合模型，并给出了分析时间属性的方法。为了刻画时间行为，他们提出了一种形式化模型称为Web 服务的时间前移系统。文献［15］也给出了另一种形式化模型，称为Web 服务的时间自动机，用于建模基于BPEL 的Web 服务的时间行为。

在文献［16］中，提出了一种BPEL 流程的形式化模型，称为μ-BPEL，它能够支持从μ-BPEL 到时间自动机的转化。

Gregorio 提出了一种时间约束条件下检查Web 服务正确性的形式化方法，他们采用WSCI语言来描述Web 服务，并将服务转换为时间自动机，然后，利用UPPAAL 工具来模拟和验证Web 服务组合的时间行为及属性;然而，该文没有给出转换为时间自动机的形式化语义。

SENSORIA 项目［2］基于SRML 语言的基础上，增加了一些新的原语用于刻画服务执行过程中可能发生的延迟。他们主要关注与时间约束相关方面包括:(1)系统的构件处理进程事件以及在其本地状态上的计算时间约束;(2)在不同对象之间传送事件的时间约束;(3)基于SOA 的中间件在执行服务的发现、选择和绑定上的时间延迟。

6 结论和未来的工作

在本文中，我们已提出了分析和验证Web 服务组合的时间属性的一种形式化框架。该框架引入了时间消息流的概念，建模了Web 服务接口的端口通信历史。为了描述Web 服务接口的时间约束，本文扩展了标准的WSDL，规范了时间约束需求。本文采用时间自动机来建模Web 服务的时间行为，多个并发时间自动机组合成一个时间自动机网络，并利用模型检测工具UPPAAL 来验证服务组合的时间属性。

在此工作基础上，将考虑Web 服务编排的时间约束需求，并应用面向服务的实时系统。另外，我们将会考虑采用其他形式化技术，例如，采用时间Petri 网来刻画和分析Web 服务的时间行为。

［1］Kaiyu Wang，Chunle Jiang. Performance Modeling And Evaluation Of Composite Web Services［J］. International Journal of Advancements in Computing Technology，2013，4(11):203 - 212.

［2］Jose Fiadeiro，Antonia Lopes，Joao Abreu. A Formal Model for Service-oriented Interactions［J］. Science of Computer Programming，2013，77(5):577 -608.

［3］Mohsen Rouached，Olivier Perrin，Claude Godart. Towards Formal Verification of Web Service Composition［C］. New York:In Proceedings of the 4th International Conference on Business Process Management，2010:257 -273.

［4］QIAN Jun-yan，HUANG Guo-wang，ZHAO Ling-zhong. Semantic Web Service Composition using Answer Set Planning［J］. International Journal of Advancements in Computing Technology，2011，3(5):20 -31.

［5］Xitong Li，Yushun Fan，Quan Z. Sheng. A Petri Net Approach to Analyzing Behavioral Compatibility and Similarity of Web Services［J］. Man and Cybernetics，2011，41(3):510 -521.

［6］ Shamim H Ripon. Process Algebraic Support for Web Service Composition［J］. ACM SIGSOFT Software Engineering Notes ，2010，35(2):1 -7.

［7］Alessandro Lapadula，Rosario Pugliese，Francesco Tiezzi. A WSDL-based Type System for Asynchronous WS-BPEL Processes［J］.Formal Methods in System Design，2011，31(4):1 -39.

［8］Gregorio Diaz，Juan-José Pardo.Verification of Web Services with Timed Automata［J］. Electronic Notes in Theoretical Computer Science，2006，157(2):19 -34.

［9］Manfred Broy，Ingolf H. Kruger，Michael Meisinger. A Formal Model of Services［J］. ACM Transactions on Software Engineering and Methodology (TOSEM)，2007，16(1):1 -40.

［10］Wolfgang Reisig. Towards a Theory of Services［J］. Information Systems and e-Business Technologies，2008，104(9):271 -281.

［11］Rajeev Alur，David L. Dill. A Theory of Timed Automata［J］.Theoretical Computer Science，1994，126(2):183 -235.

［12］Raman Kazhamiakin，Paritosh Pandya，Marco Pistore. Timed Modelling and Analysis in Web Service Compositions［C］. Shanghai:The First International Conference on Availability，Reliability and Security (ARES)，2011:840 -846.

［13］Gerd Behrmann，Alexandre David，Kim G. Larsen. A Tutorial on UPPAAL［J］. Formal Methods for the Design of Real-time Systems，2004，12(2):200 -234.

［14］Howard Foster，Sebastian Uchitel，Jeff Magee. A Tool for Modelbased Verification of Web Service Compositions and Choreography［C］.BeiJing:In Proceedings of the 28th International Conference on Software Engineering，2006:771 -774.

［15］Jia Mei，Huaikou Miao，Qingguo Xu，et al. Modeling and Verifying Web Service Applications with Time Constraints［C］.Shanghai:International Conference on Computer and Information Science，2010:791 -795.

［16］Pu Geguang，Zhao Xiangpeng，Wang Shuling，et al. Towards the Semantics and Verification of BPEL4WS［J］. Electronic Notes in Theoretical Computer Science，2006，151(2):3 -52.