王雪紅，劉柯威，陳冠萍，胡元闖

（賀州學(xué)院計算機科學(xué)與信息工程學(xué)院，廣西賀州542899）

基于時間擴展的Web服務(wù)模型檢測

王雪紅，劉柯威，陳冠萍，胡元闖

（賀州學(xué)院計算機科學(xué)與信息工程學(xué)院，廣西賀州542899）

由于傳統(tǒng)的形式化方法不能保證帶時間約束的組合Web服務(wù)安全可靠地運行，為了有效地分析并確保帶時間約束的組合Web服務(wù)的正確性，利用時間自動機驗證工具UPPAAL將帶時間約束的組合Web服務(wù)的每個原子服務(wù)建立自動機模型，給出ASEHA語義描述，并用模擬器模擬帶時間約束的Web服務(wù)的運行過程，對帶有時間約束的Web服務(wù)的屬性進行分析。最后，以旅行預(yù)訂票組合系統(tǒng)為例，驗證其死鎖、活性和安全性。實例證明此方法有效。

Web服務(wù)；ASEHA；時鐘約束；UPPAAL

組合Web服務(wù)為了適應(yīng)各種應(yīng)用的約束環(huán)境，導(dǎo)致在信息互換過程中易產(chǎn)生繁多信息流，如何確保每個業(yè)務(wù)流正確、實時地完成任務(wù)顯得十分重要。為了適應(yīng)帶時間約束的組合Web服務(wù)系統(tǒng)的建模與驗證需求，R.Alur等［1］在有限狀態(tài)機的基礎(chǔ)上提出了時間自動機理論；駱翔宇等［2］基于時間自動機理論，對Web服務(wù)模型進行檢測；吳瓊等［3］基于一種著色時間Petri網(wǎng)對實時系統(tǒng)進行形化建模，最后利用模型驗證UPPAAL工具對系統(tǒng)的性質(zhì)進行分析。

1 案例分析

1.1 問題描述

旅行預(yù)訂票系統(tǒng)是一個帶時間約束的組合Web服務(wù)，它由旅行者（Traveler）、旅行代理（TravelAgent）及航空公司預(yù)訂票（AirlineReservation）三個服務(wù)構(gòu)成。Web服務(wù)系統(tǒng)的運行是從旅行者模型開始。如果旅游者計劃旅行，那么他首先通過旅行者系統(tǒng)將旅行計劃路線提交給旅行代理系統(tǒng)，旅行代理系統(tǒng)根據(jù)接收的旅行路程線路來選擇最佳旅行的線路。旅行代理系統(tǒng)針對每條旅行的線路，通過航空公司預(yù)訂票系統(tǒng)查詢航班號，并檢查該航班是否有座位。在這個過程中，旅行者可以有選擇地同意或取消航空公司預(yù)訂票系統(tǒng)所提供的服務(wù)。當旅行者同意了航空公司預(yù)訂票系統(tǒng)所提供的航班服務(wù)時，此次預(yù)定只在24小時以內(nèi)有效，如果旅行者超過24小時未發(fā)送訂票確認“Book Tickets”消息，則航空公司預(yù)訂票系統(tǒng)會自動取消此次預(yù)訂。

（1）如果旅行者取消了航空預(yù)訂票系統(tǒng)所提供的航班服務(wù)，那么他需給出期望的航班號，并等待旅行代理系統(tǒng)的應(yīng)答；

（2）如果旅行者取消了此次旅行，他將發(fā)送“Cancel Reservation”消息給旅行代理系統(tǒng)，以取消此次預(yù)定；

（3）如果旅行者同意了航空公司預(yù)訂票系統(tǒng)所提供的航班服務(wù)，他將發(fā)送“Reserve Tickets”消息給旅行代理系統(tǒng)，并通過網(wǎng)上銀行等途經(jīng)支付機票金額，從而完成機票的預(yù)定。

1.2 旅行預(yù)訂票組合Web服務(wù)建模

旅行預(yù)訂票組合Web服務(wù)的消息交互如圖1所示。

圖1 旅行預(yù)訂票Web服務(wù)系統(tǒng)消息交互

旅行者預(yù)定機票的Web服務(wù)系統(tǒng)W0由旅行者（Traveler）、旅行代理（TravelAgent）及航空公司預(yù)訂票（AirlineReservation）三個自動機模型構(gòu)成，它們之間的關(guān)系是and-關(guān)系。采用UPPAAL工具中的編輯器將旅游預(yù)訂票Web服務(wù)系統(tǒng)的三個原子服務(wù)建立為基于時間擴展的ASEHA自動機模型，如圖2所示。

圖2 旅行預(yù)訂票Web服務(wù)系統(tǒng)模型

1.3 旅行預(yù)訂票組合Web服務(wù)語義分析

下面給出該組合Web服務(wù)系統(tǒng)旅行者（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自動機狀態(tài)的集合；I=t0是初始狀態(tài)；Γ=｛x｝是時鐘有限集合；Λ=｛10，11，12，L，1n｝是遷移標記的集合；L是｛t0，t1，t2，…，t8｝中時鐘約束值的狀態(tài)的映射，其中ti=0，1，…T，8； F=t0是終態(tài)；→?Σ×Λ×Σ=｛（x，y，z）｜x∈Σ∧y∈Λ∧z∈Σ｝是遷移關(guān)系。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）和航空公司預(yù)訂票（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 旅行預(yù)訂票組合Web服務(wù)驗證與分析

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語法進行性質(zhì)驗證，BNF語法如下：

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

為了驗證旅行預(yù)訂票組合Web服務(wù)模型的安全可靠性，使用屬性驗證對模型的需求規(guī)范進行驗證與分析，部分模擬路徑軌跡如圖3所示。

圖3 部分模擬路徑軌跡

下面利用時態(tài)邏輯來表述其屬性。

（1）死鎖。A［］not deadlock：驗證結(jié)果為true，表明該模型在運行過程中不會出現(xiàn)死鎖現(xiàn)象。

（2）安全性。安全性是指所建立的形式化模型需要滿足設(shè)計者的若干安全限制。在該Web服務(wù)系統(tǒng)模型實例中安全性要求主要有以下幾個方面：

1）如果旅行者請求旅行代理訂票，則旅行代理必須在規(guī)定的時間內(nèi)向航空公司發(fā)出請求，屬性為：A［］TravelAgent.BookOk imply Airline.x＜24，通過驗證，驗證結(jié)果為true。

2）旅行代理必須允許旅行者修改旅程服務(wù)，屬性為：A［］Traveler.ChangeItinerary imply Travel Agent.CheckSeats，通過驗證，結(jié)果為true。

3）旅行代理必須發(fā)送旅行者需求旅程服務(wù)，屬性為：A［］Traveler.Itinerary imply Travel Agent. Cgent.CheckSears，通過驗證，結(jié)果為true。

4）在訂票前旅行代理允許旅行者取消旅程服務(wù)，屬性為：A［］Traveler.CancelReserve implyTravelaAgent.CancelOk，通過驗證，結(jié)果為true。

（3）活性。假如旅行者發(fā)送訂票請求，并在24小時內(nèi)確認訂票，航空公司必須接受請求并完成訂票進程，屬性為：A＜＞（（Traveler.BookTicket and Airline.x＜24）imply Airline.FinishBookSeat），通過驗證，結(jié)束為true。

2 結(jié)語

本文介紹了一種帶有時間擴展的ASEHA模型檢測技術(shù)對組合Web服務(wù)進行驗證的方法，分析了旅行預(yù)訂票Web服務(wù)系統(tǒng)。提出基于帶時間約束的異步擴展層次自動機計算模型，利用模型驗證工具UPPAAL對該系統(tǒng)進行驗證與分析，驗證了其死鎖、安全性、活性等屬性。實例驗證表明了該方法的有效性。下一步的工作考慮如何將模型檢測和定理證明相結(jié)合對組合Web服務(wù)進行形式化驗證。

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

［2］駱翔宇,軒愛成,沙宗魯.基于時間自動機的Web服務(wù)模型檢測［J］.計算機科學(xué),2010,37（8）:139-142.

［3］吳瓊,邵志清,劉剛,等.基于著色時間Petri網(wǎng)的實時系統(tǒng)的形式驗證［J］.計算機科學(xué),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

廣西自然科學(xué)基金資助項目（2014jjBA70066）；賀州學(xué)院校級科研項目（2014ZC22）；賀州學(xué)院校級教改項目（hzxyjg201514，hzxyjg201515）

王雪紅（1983-），女，河南濮陽人，賀州學(xué)院講師。