基于时间扩展的Web服务模型检测

王雪红，刘柯威，陈冠萍，胡元闯

（贺州学院计算机科学与信息工程学院，广西贺州542899）

基于时间扩展的Web服务模型检测

王雪红，刘柯威，陈冠萍，胡元闯

（贺州学院计算机科学与信息工程学院，广西贺州542899）

由于传统的形式化方法不能保证带时间约束的组合Web服务安全可靠地运行，为了有效地分析并确保带时间约束的组合Web服务的正确性，利用时间自动机验证工具UPPAAL将带时间约束的组合Web服务的每个原子服务建立自动机模型，给出ASEHA语义描述，并用模拟器模拟带时间约束的Web服务的运行过程，对带有时间约束的Web服务的属性进行分析。最后，以旅行预订票组合系统为例，验证其死锁、活性和安全性。实例证明此方法有效。

Web服务；ASEHA；时钟约束；UPPAAL

组合Web服务为了适应各种应用的约束环境，导致在信息互换过程中易产生繁多信息流，如何确保每个业务流正确、实时地完成任务显得十分重要。为了适应带时间约束的组合Web服务系统的建模与验证需求，R.Alur等［1］在有限状态机的基础上提出了时间自动机理论；骆翔宇等［2］基于时间自动机理论，对Web服务模型进行检测；吴琼等［3］基于一种着色时间Petri网对实时系统进行形化建模，最后利用模型验证UPPAAL工具对系统的性质进行分析。

1 案例分析

1.1 问题描述

旅行预订票系统是一个带时间约束的组合Web服务，它由旅行者（Traveler）、旅行代理（TravelAgent）及航空公司预订票（AirlineReservation）三个服务构成。Web服务系统的运行是从旅行者模型开始。如果旅游者计划旅行，那么他首先通过旅行者系统将旅行计划路线提交给旅行代理系统，旅行代理系统根据接收的旅行路程线路来选择最佳旅行的线路。旅行代理系统针对每条旅行的线路，通过航空公司预订票系统查询航班号，并检查该航班是否有座位。在这个过程中，旅行者可以有选择地同意或取消航空公司预订票系统所提供的服务。当旅行者同意了航空公司预订票系统所提供的航班服务时，此次预定只在24小时以内有效，如果旅行者超过24小时未发送订票确认“Book Tickets”消息，则航空公司预订票系统会自动取消此次预订。

（1）如果旅行者取消了航空预订票系统所提供的航班服务，那么他需给出期望的航班号，并等待旅行代理系统的应答；

（2）如果旅行者取消了此次旅行，他将发送“Cancel Reservation”消息给旅行代理系统，以取消此次预定；

（3）如果旅行者同意了航空公司预订票系统所提供的航班服务，他将发送“Reserve Tickets”消息给旅行代理系统，并通过网上银行等途经支付机票金额，从而完成机票的预定。

1.2 旅行预订票组合Web服务建模

旅行预订票组合Web服务的消息交互如图1所示。

图1 旅行预订票Web服务系统消息交互

旅行者预定机票的Web服务系统W0由旅行者（Traveler）、旅行代理（TravelAgent）及航空公司预订票（AirlineReservation）三个自动机模型构成，它们之间的关系是and-关系。采用UPPAAL工具中的编辑器将旅游预订票Web服务系统的三个原子服务建立为基于时间扩展的ASEHA自动机模型，如图2所示。

图2 旅行预订票Web服务系统模型

1.3 旅行预订票组合Web服务语义分析

下面给出该组合Web服务系统旅行者（Traveler）的时间扩展的ASEHA自动机给出Traveler，该框架由七元组进行定义，H=（Au，m，ω，β，f，var，Ψ），其中：

（1）Au=｛Traveler，TravelAgent，AirlineReservation，C，D，E｝， 其 中 ，C，D，E∈AirlineReservation。 Traveler由七元组定义，，其中：

Ω=｛t0，t1，t2，…，t8｝是Traveler自动机状态的集合；I=t0是初始状态；Γ=｛x｝是时钟有限集合；Λ=｛10，11，12，L，1n｝是迁移标记的集合；L是｛t0，t1，t2，…，t8｝中时钟约束值的状态的映射，其中ti=0，1，…T，8； F=t0是终态；→⊆Σ×Λ×Σ=｛（x，y，z）｜x∈Σ∧y∈Λ∧z∈Σ｝是迁移关系。Traveler自动机的部分迁移：ΛTraveler=｛（t0，（true，put（ordertrip），Ø），t1），（t1，（true，get（no_available），Ø），t0)，（t1，（true，（ge（tavailable），Ø），t2），…，（t8，（true,ge（treceive_tickets），Ø），t0）｝；

（2）m=｛no_available,ordertrip,available,change_itinerary,cancel_itinerary,Reserve_tickets, no_reservation,notify_timeout,book_ticket,cancel_reservation,receive_statement,receive_tickets, accept_cancel｝；

旅行代理（TravelAgent）和航空公司预订票（AirlineReservation）自动机模型的定义与旅行者（Traveler）类似；

（3）ω=｛T，Tl，AR｝；

（4）β（ω0）＝｛C，D，E｝；

（5）（fTraveler）＝T，（fTravelAgent）＝Tl，（fAR）＝AirlineReservation；

（6）var＝（u，v，x）；

1.4 旅行预订票组合Web服务验证与分析

1.4.1 UPPAAL介绍

本文使用UPPAAL模型验证工具进行模拟实验。有以下几种形式的约束：g::＝g,g—g_data—g_clock，其中：1）g_data::＝ex＜ex—ex＜＝ex—ex＝＝ex—ex＞＝ex—ex＞ex；ex::＝n—ex＋ex—v[ex]—ex-ex—ex*ex—ex/ex—（g_data?ex,ex）；2）g_clock::＝x＜n—x＜＝n—x＝＝n—x＞＝n—x＞n。

1.4.2 属性验证与分析

时间模型验证工具UPPAAL使用BNF语法进行性质验证，BNF语法如下：

Prop::＝A［］p—E＜＞p—E＜＞p—A＜＞p—p-＞p

为了验证旅行预订票组合Web服务模型的安全可靠性，使用属性验证对模型的需求规范进行验证与分析，部分模拟路径轨迹如图3所示。

图3 部分模拟路径轨迹

下面利用时态逻辑来表述其属性。

（1）死锁。A［］not deadlock：验证结果为true，表明该模型在运行过程中不会出现死锁现象。

（2）安全性。安全性是指所建立的形式化模型需要满足设计者的若干安全限制。在该Web服务系统模型实例中安全性要求主要有以下几个方面：

1）如果旅行者请求旅行代理订票，则旅行代理必须在规定的时间内向航空公司发出请求，属性为：A［］TravelAgent.BookOk imply Airline.x＜24，通过验证，验证结果为true。

2）旅行代理必须允许旅行者修改旅程服务，属性为：A［］Traveler.ChangeItinerary imply Travel Agent.CheckSeats，通过验证，结果为true。

3）旅行代理必须发送旅行者需求旅程服务，属性为：A［］Traveler.Itinerary imply Travel Agent. Cgent.CheckSears，通过验证，结果为true。

4）在订票前旅行代理允许旅行者取消旅程服务，属性为：A［］Traveler.CancelReserve implyTravelaAgent.CancelOk，通过验证，结果为true。

（3）活性。假如旅行者发送订票请求，并在24小时内确认订票，航空公司必须接受请求并完成订票进程，属性为：A＜＞（（Traveler.BookTicket and Airline.x＜24）imply Airline.FinishBookSeat），通过验证，结束为true。

2 结语

本文介绍了一种带有时间扩展的ASEHA模型检测技术对组合Web服务进行验证的方法，分析了旅行预订票Web服务系统。提出基于带时间约束的异步扩展层次自动机计算模型，利用模型验证工具UPPAAL对该系统进行验证与分析，验证了其死锁、安全性、活性等属性。实例验证表明了该方法的有效性。下一步的工作考虑如何将模型检测和定理证明相结合对组合Web服务进行形式化验证。

［1］ALUR R,DILLD.Atheoryoftimed automata［J］.Theoretical Computer Science,1994,126（2）:183-235.

［2］骆翔宇,轩爱成,沙宗鲁.基于时间自动机的Web服务模型检测［J］.计算机科学,2010,37（8）:139-142.

［3］吴琼,邵志清,刘刚,等.基于着色时间Petri网的实时系统的形式验证［J］.计算机科学,2008,35（7）:257-260.

【责任编辑：王桂珍 foshanwgzh@163.com】

Model checking Web services based on timed extension

WANGXue-hong,LIUKe-wei,CHENGuan-ping,HUYuan-chuang
（College ofComputer Science and Information Technology,Hezhou University,Hezhou 542899,China）

As the traditional formal methods can not guarantee safe and reliable operation of Web services composition with timed constraints,each atom service of Web services composition with timed constraints built automata model using the model checker UPPAAL,and gave ASEHA semantic description in order to analyze and ensure the correctness ofWeb services composition with timed constraints.Runningprocess ofWeb services composition with timed constraints was simulated by simulator of UPPAAL.We analyzed the properties of Web services composition with timed constraints.Finally,we verified properties of deadlock,liveness and security such as the travel reservation system.An example was provided to demonstrate the modeling process and formal verification.

Web services;ASEHA;clock constraints;UPPAAL

TP393.09

A

1008-0171（2017）02-0014-04

2016-11-18

广西自然科学基金资助项目（2014jjBA70066）；贺州学院校级科研项目（2014ZC22）；贺州学院校级教改项目（hzxyjg201514，hzxyjg201515）

王雪红（1983-），女，河南濮阳人，贺州学院讲师。