摘 要：基于時(shí)間擴(kuò)展的ASEHA自動(dòng)機(jī)理論，以旅行預(yù)訂票組合Web服務(wù)為例，分別建立了旅行者（Traveler）、旅行代理（Travel Agent）及航空公司預(yù)訂票（Airline Reservation）三個(gè)自動(dòng)機(jī)，并給出該服務(wù)的BPEL語(yǔ)言描述。

關(guān)鍵詞：組合Web服務(wù)；ASEHA；BPEL

中圖分類(lèi)號(hào)：TP301.1

為了保證組合Web服務(wù)的安全運(yùn)行，建模技術(shù)是關(guān)鍵的技術(shù)之一[1]。雖然組合Web服務(wù)技術(shù)滿(mǎn)足了各種企業(yè)的應(yīng)用程序的集成，但是在多個(gè)業(yè)務(wù)流程組合的過(guò)程會(huì)產(chǎn)生大量復(fù)雜的信息交互。因此如何保證各種業(yè)務(wù)流程正確、可靠和安全的執(zhí)行顯得尤為重要。直今為止，時(shí)間自動(dòng)機(jī)理論在實(shí)時(shí)系統(tǒng)建模與驗(yàn)證、自動(dòng)驗(yàn)證工具的研發(fā)及整個(gè)模型檢測(cè)領(lǐng)域占有很重要的位置。

本文第2節(jié)給出了一種帶有時(shí)間約束的異步擴(kuò)展層次自動(dòng)機(jī)相關(guān)概念；第3節(jié)以旅行預(yù)訂票組合Web服務(wù)系統(tǒng)為例，建立基于時(shí)間擴(kuò)展的ASEHA模型，并給其BPEL語(yǔ)言描述；最后對(duì)全文進(jìn)行總結(jié)。

1 相關(guān)概念和定義

基于Ramsokul[2-3]博士所提出的ASEHA （Asynchronous Extended Hierarchical Automata） 模型，本節(jié)將引入了時(shí)鐘變量，在遷移上增加了時(shí)鐘約束，拓展了ASEHA的語(yǔ)義。它由七元組來(lái)定義H=（Au，m，ω，β，f，var，Ψ）。

定義1 （帶時(shí)鐘約束的遷移） 本文在此基礎(chǔ)之上引入了reset，guard，遷移定義為，遷移的標(biāo)簽為，由五元組（tr，ac，td，reset，guard）來(lái)定義。其中，tr是觸發(fā)；ac是活動(dòng)令牌；是目標(biāo)限定詞；是復(fù)位的時(shí)鐘集；是時(shí)鐘使能條件。

定義2（格局）一個(gè)格局是指H中處于活動(dòng)狀態(tài)的集合。比如集合是一個(gè)格局，當(dāng)且僅當(dāng)：

①任何一個(gè)自動(dòng)機(jī)最多只有一個(gè)狀態(tài)為格局，比如：；

②向上封閉：如果一個(gè)狀態(tài)s屬于C，那么s的父狀態(tài)也屬于C。

定義3 （觸發(fā)） 對(duì)于遷移，tr是由變量和狀態(tài)定義的布爾謂詞組合。謂詞由∧、∨和﹁連接，src和dest分別表示活動(dòng)狀態(tài)和目標(biāo)狀態(tài)。

2 案例分析

旅行者預(yù)定機(jī)票的Web服務(wù)系統(tǒng)由旅行者（Traveler）、旅行代理（Travel Agent）及航空公司預(yù)訂票（Airline Reservation）三個(gè)自動(dòng)機(jī)模型構(gòu)成，它們的之間的關(guān)系是and-關(guān)系。如圖1所示。

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

面向Web服務(wù)的業(yè)務(wù)流程執(zhí)行語(yǔ)言BPEL或BPEL4WS（Business Process Execution Language For Web Services）是一種使用Web定義和執(zhí)行業(yè)務(wù)流程的語(yǔ)言。BPEL中的每一個(gè)組件都可以在基于ASEHA自動(dòng)機(jī)中找到與此對(duì)應(yīng)的元素?；跁r(shí)間擴(kuò)展的ASEHA自動(dòng)機(jī)是一系列流程的集合，而流程是時(shí)間擴(kuò)展的ASEHA的基本組成成分，它包括了各個(gè)組成部分的行為。BPEL中活動(dòng)的序列、活動(dòng)選擇操作、流程調(diào)用中的并行操作及活動(dòng)的時(shí)間約束等都能夠依次被時(shí)間擴(kuò)展的ASEHA自動(dòng)機(jī)中的狀態(tài)遷移、選擇權(quán)、并行流程及時(shí)間變量的約束來(lái)表示。

下面給出旅游預(yù)訂票Web服務(wù)系統(tǒng)的部分BPEL描述語(yǔ)言：

…

role=“tns： TravelAgent System”

operation=“tns： TAtoAirlineReservation/AcceptCancellation”>

role=“tns： TravelAgent System”

operation=“tns： TAtotraveler/NotifyofCancellation”/>

…

…

3 結(jié)束語(yǔ)

本文對(duì)旅行預(yù)訂票組合Web服務(wù)系統(tǒng)進(jìn)行分析，該系統(tǒng)包含旅行者（Traveler），旅行代理（TravelAgent）及航空公司預(yù)訂票（AirlineReservation）三個(gè)原子服務(wù)的消息交互，分別對(duì)這三個(gè)原子服務(wù)建立形式化模型。最后，對(duì)其進(jìn)行BPEL語(yǔ)言描述。在本文的基礎(chǔ)上，下一步的工作是對(duì)其系統(tǒng)進(jìn)行屬性驗(yàn)證。

參考文獻(xiàn)：

[1]劉如娟，戴桂蘭，胡長(zhǎng)軍，白曉穎.Web服務(wù)的模型檢測(cè)技術(shù)探討[J].小型微型計(jì)算機(jī)系統(tǒng)，2007（11）：1921-1927.

[2]PAMSOKUL P，SOWMYA A.ASEHA： a web services protocol modeling formalism[C]//4th IEEE Int’l Conference on Software Engineering and Formal Methods （to appear）.IEEE Computer Society，2006：1-25.

[3]PAMSOKUL P，SOWMYA A.Sniffer based approach to web services protocol conformance checking[C]//5th Int’l Symposium on Parallel and Distributed Computing （ISPDC），Timisoara，Romania，IEEE Computer Society，2006：58-65.

作者簡(jiǎn)介：王雪紅（1983-），女，河南濮陽(yáng)人，助教，碩士研究生，主要研究方向：實(shí)時(shí)系統(tǒng)、模型檢測(cè)。

作者單位：賀州學(xué)院 計(jì)算機(jī)科學(xué)與信息工程學(xué)院，廣西賀州 542899；武漢大學(xué) 計(jì)算機(jī)學(xué)院，武漢 430072

基金項(xiàng)目：本文受廣西高等學(xué)校立項(xiàng)科研項(xiàng)目（項(xiàng)目編號(hào)：201204LX461），賀州學(xué)院校級(jí)科研項(xiàng)目（項(xiàng)目編號(hào)：2012ZRKY07），賀州學(xué)院校級(jí)科研項(xiàng)目（項(xiàng)目編號(hào)：2012ZRKY06）資助。