基于時(shí)間擴(kuò)展的Web服務(wù)模型檢測(cè)

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

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

基于時(shí)間擴(kuò)展的Web服務(wù)模型檢測(cè)

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

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

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

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

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

1 案例分析

1.1 問題描述

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

（1）如果旅行者取消了航空預(yù)訂票系統(tǒng)所提供的航班服務(wù)，那么他需給出期望的航班號(hào)，并等待旅行代理系統(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)支付機(jī)票金額，從而完成機(jī)票的預(yù)定。

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

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

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

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

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

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

下面給出該組合Web服務(wù)系統(tǒng)旅行者（Traveler）的時(shí)間擴(kuò)展的ASEHA自動(dòng)機(jī)給出Traveler，該框架由七元組進(jìn)行定義，H=（Au，m，ω，β，f，var，Ψ），其中：

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

Ω=｛t0，t1，t2，…，t8｝是Traveler自動(dòng)機(jī)狀態(tài)的集合；I=t0是初始狀態(tài)；Γ=｛x｝是時(shí)鐘有限集合；Λ=｛10，11，12，L，1n｝是遷移標(biāo)記的集合；L是｛t0，t1，t2，…，t8｝中時(shí)鐘約束值的狀態(tài)的映射，其中ti=0，1，…T，8； F=t0是終態(tài)；→?Σ×Λ×Σ=｛（x，y，z）｜x∈Σ∧y∈Λ∧z∈Σ｝是遷移關(guān)系。Traveler自動(dòng)機(jī)的部分遷移：Λ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）自動(dòng)機(jī)模型的定義與旅行者（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ù)驗(yàn)證與分析

1.4.1 UPPAAL介紹

本文使用UPPAAL模型驗(yàn)證工具進(jìn)行模擬實(shí)驗(yàn)。有以下幾種形式的約束：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 屬性驗(yàn)證與分析

時(shí)間模型驗(yàn)證工具UPPAAL使用BNF語法進(jìn)行性質(zhì)驗(yàn)證，BNF語法如下：

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

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

圖3 部分模擬路徑軌跡

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

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

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

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

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

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

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

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

2 結(jié)語

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

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

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

［3］吳瓊,邵志清,劉剛,等.基于著色時(shí)間Petri網(wǎng)的實(shí)時(shí)系統(tǒng)的形式驗(yàn)證［J］.計(jì)算機(jī)科學(xué),2008,35（7）:257-260.

【責(zé)任編輯：王桂珍 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é)基金資助項(xiàng)目（2014jjBA70066）；賀州學(xué)院校級(jí)科研項(xiàng)目（2014ZC22）；賀州學(xué)院校級(jí)教改項(xiàng)目（hzxyjg201514，hzxyjg201515）

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