時間約束條件下Web 服務組合的形式化分析與驗證＊

陳志輝 ，吳敏敏

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

在分布式計算和電子商務中，面向服務計算(Service-Oriented Computing，SOC)已成為一個典型的應用范例［1］，它將可用的服務通過組合的方式來快速構(gòu)建復雜的應用。Web 服務應用就是采用SOC 的思想:首先，可用的服務是基于標準的Web 服務定義語言(Web Services Description Language ，WSDL)來描述;然后，通過服務組合語言(如BPEL，WSCI 和OWL-S)來實現(xiàn)功能更復雜的服務，稱為復合服務［2］。

雖然服務組合語言可描述Web 服務之間的交互行為，但缺少形式化方法來驗證Web 服務的行為屬性。為此，研究人員已提出一些形式化驗證方法。例如，Mohsen R 提出了一種基于事件驅(qū)動的方法來驗證Web 服務組合［3］，采用BPEL 流程來定義Web 服務組合，而事件演算(EC)用于刻畫服務的行為屬性。除了事件演算，還有其他形式化的方法，如有限狀態(tài)機(FSM)［4］、Petri 網(wǎng)［5］、進程代數(shù)［6］、類型系統(tǒng)［7］等。

然而，Web 服務組合的正確性檢查也包括非功能性需求，如響應時間、性能等。在電子商務應用當中，許多業(yè)務場景都有實時性要求，即在一定的時間約束條件下，系統(tǒng)必須完成相應的任務。例如，銀行的電子轉(zhuǎn)賬無法準時到達對方賬戶，這可能給商家?guī)砭薮蟮慕?jīng)濟損失［8］。

為此，本文將描述如何使用模型檢查技術(shù)以驗證Web 服務的時間行為屬性。在Web 服務技術(shù)領域，服務之間的調(diào)用是通過消息的方式，即發(fā)送和接收消息。一方面，執(zhí)行操作調(diào)用需耗費一定的時間。另一方面，傳遞消息也需要一段時間。例如，由于通信網(wǎng)絡中斷，客戶端就會無期限地等待服務響應。這種情況下，應該設置服務響應的時間約束。因而，本文擴展了標準的WSDL，增加了時間約束語句來描述Web 服務接口，一個時間自動機用于刻畫單個服務接口的時間行為，服務組合可看作是由這些時間自動機所組成的網(wǎng)絡，并通過模型檢查工具UPPAAL 來自動驗證時間的行為屬性。

1 案例研究

文中借助提出的一個股票分析案例作為應用場景展開分析，并給出具體建模過程與驗證。該應用主要涉及四個服務:股票代理服務(SBS)看作是一個經(jīng)紀人，他為投資者提供股票投資評估服務;實現(xiàn)SBS 是一個服務組合過程，它與股票研究服務(SRS)和投資管理服務(IMS)之間進行交互;SRS 是由不同的證券公司所提供的服務，包括數(shù)據(jù)庫維護、股票前景預測、股票配置等;IMS 維護投資者相關個人信息數(shù)據(jù)庫;用戶交互服務(UIS)提供訪問接口功能。通常的流程是，SBS 接收到從UIS發(fā)送過來的股票分析請求，經(jīng)過IMS 驗證投資者的個人信息，通過SRS 確認股票投資的可行性。最后，SBS 給投資者提供了一份關于股票投資的可行性研究報告。

除了上述功能需求部分，服務組合的執(zhí)行過程中必須滿足的時間約束。在一些實時性要求高的業(yè)務領域(如股市)可能包含下列的時間約束條件:(1)在投資者決定訪問SBS 后，UIS 應該在10個時間單位內(nèi)將請求發(fā)送到SBS;(2)在IMS 接收到由SBS 發(fā)送過來的請求后，驗證投資者的身份信息不超過8 個時間單位;(3)SRS 向SBS 提供投資可行性研究報告時，必須在20 個時間單位內(nèi)完成。

服務組合過程中也要滿足上述的時間約束。例如，如果投資者無法在規(guī)定的時間內(nèi)獲得股票投資研究報告，那么整個過程就會失去它的商業(yè)價值。此外，還存在這樣的情況，即時間約束和服務組合不一致。在上述場景中，各個服務之間的通信時間也應考慮。例如，UIS 應在10 個時間單位內(nèi)發(fā)送一個請求到SBS。但是，由于網(wǎng)絡中斷，該請求就無法到達它的目的地。

為了驗證服務的時間屬性，首先需對Web 服務建模時間行為。在接下來，文中將擴展Web 服務接口的時間約束規(guī)范，采用時間自動機來建模Web 服務的時間行為，并使用模型檢查技術(shù)來自動驗證服務的時間屬性。

2 Web 服務

Web 服務是一個自描述的和獨立的軟件實體，它利用標準的語言和協(xié)議在互聯(lián)網(wǎng)上進行發(fā)布、發(fā)現(xiàn)和調(diào)用［9］。其中一個關鍵技術(shù)就是Web服務描述語言WSDL，將服務看作為一個抽象的端口集合。WSDL 還定義了Web 服務以何種動作來傳送數(shù)據(jù)。一個動作就是一個操作，數(shù)據(jù)由消息來表示。相關操作的集合稱為一個端口類型。端口類型就是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 用于規(guī)范從接收一個input message 到發(fā)送一個output message 的時間單元值。

＜operation name="getAuthenti

cation" ＞

＜inputname ="getAuthentica

tionRequest"/ ＞

＜outputname ="getAuthenti

cationResponse”/)

＜constraint duration=10/)

＜/operation ＞

上面例子的第4 行中，duration 定義了從接收“getAuthenticationRequest”到發(fā)送“getAuthenticationResponse”消息必須在10 個時間單元之內(nèi)。如果在一個message 有時間約束，那么transmission-Time 用于規(guī)范該消息message 必須發(fā)送到目標的時間單元值。

＜message name="getAuthentication" ＞

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

＜constraint transmissionTime ＜=5/ ＞

＜/message ＞

在上面例子的第3 行中，transmissionTime 定義了傳送“getAuthenticationRequest”的時間不超過5個時間單位。

2.1 Web 服務的形式化模型

一般地，Web 服務模型是由其外部可觀察到行為組成的，它通過服務端口來發(fā)送或接收消息，以此方式與外部環(huán)境進行通信。為了建模這些端口的通信行為，本文引入了在FOCUS 框架中消息流的概念［10］。消息流是一個有限的或無限的消息而組成的序列?？紤]到Web 服務的時間行為，將時間幀加入消息流中，則稱為時間消息流，其定義如下:

(2)為了實現(xiàn)高密度，采用了靶丸注入和分子束、中性束注入。而靶丸注入和超聲分子束注入會降低溫度，入射深度也有問題。

定義1(時間消息流) 給定的一組消息M，一個時間消息流＜t，ms ＞是由時間幀t 和一個消息序列ms ∈M*組成的，其中M*是一個有限消息序列組成的集合。

時間消息流是表示在一個特定的時間幀內(nèi)，Web 服務與環(huán)境之間的通信行為。在本文中，時間幀是由一個離散時間的符號來表示，即自然數(shù)N。

Web 服務接口是由端口來描述的，如圖1 所示，服務通過這些端口與環(huán)境進行通信。端口是有方向性的(例如:輸入或輸出端口)和類型的(例如:端口類型規(guī)范了什么樣的信息可以由這個端口發(fā)送或接收)。

圖1 Web 服務與環(huán)境進行通信的模型

定義2(接口) 一個接口〈I，O〉是由輸入端口集合I 和輸出端口集合O 組成的，并且I ∩O = φ;每個端口〈p，MP〉∈I ∪O 包括一個端口的標識符(或名稱)和一組消息MP?M，這些消息可以通過該端口發(fā)送和接收。

定義3(接口類型) 給定一個服務接口〈I，O〉，輸入端口集I(輸出端口集O)的類型表示為TI=Type(I)(或TO= Type(O))，那么它的類型是一個函數(shù)類型:TI→TO。

消息流的概念可用來定義端口歷史，一個端口歷史是由在該端口上通信的消息而產(chǎn)生的。

定義4(端口歷史) 給定一個端口集合P，一個端口歷史可看作是從每個端口標識符p ∈P 到消息流〈tp，msp〉的一個映射。^P 表示P 中所有端口歷史的集合。定義5(執(zhí)行) 給定一個接口〈I，O〉，服務的執(zhí)行e ∈(^I ∪^O)，是屬于在該接口下某一個端口歷史。

定義6(行為) 給定一個接口〈I，O〉，服務的行為B ?(^I ∪^O)，是屬于在該接口下的某一個端口歷史集合。

由于一個服務行為可看作是輸入和輸出端口歷史之間的關系，則將它定義為一個函數(shù)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)表示W(wǎng)eb 服務接口〈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)。為了確認該服務組合是否滿足時序約束的需求，接下來將先建模每個服務的時間行為，再通過模型檢查技術(shù)來驗證服務組合的時間屬性。

3 時間自動機

時間自動機之間通過共享信道進行同步，但不能支持傳值通信。為此，可以通過共享變量的方式來實現(xiàn)同步傳值通信，首先由輸出方給一個共享變量賦值，之后輸入方再直接訪問該共享變量，獲得數(shù)值。時間自動機是一種用于描述、分析實時系統(tǒng)行為的形式化模型［11］。它是在傳統(tǒng)的有限狀態(tài)機的基礎上增加了時鐘變量和時鐘約束，用于刻畫連續(xù)變化的時間。時間自動機的語義被定義為一個標記遷移系統(tǒng)［12］。

給定一個時鐘集合X，D(X)為定義在X 上的時鐘約束集合，其語法定義如下:

其中，x ∈X，c ∈N，r ∈{＜，≤，=，＞，≥}。定義9(時間自動機) 一個時間自動機可以用一個八元組(S，S0，F(xiàn)，I，O，X，E，Inv)來表示，其中:

(1)S 是一個有限狀態(tài)集;

(2)S0∈S 是初始狀態(tài);

(3)F ?S 是一個結(jié)束狀態(tài)集;

(4)I 是一個輸入端口集(或輸入動作集);

(5)O 是一個輸出端口集(或輸出操作集);

(6)X 是時鐘變量的集合

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

(8)Inv:S →D(X)是一個映射，為S 中的每一個狀態(tài)指定D(X)中的某一個約束。

在服務交互過程中，一個狀態(tài)遷移＜s，a，g，r，s' ＞∈E 可寫為，它表示在保證時間約束條件g 為真的條件下，狀態(tài)s 遷移到s' ，執(zhí)行了通信動作a ∈I ∪O 或內(nèi)部動作τ，并重設時鐘變量r 為0。時鐘賦值是通過一個函數(shù)f:X →R+，表示將時鐘集合X 映射為非負實數(shù);Rc表示時鐘賦值的集合;f ∈Inv(s)表示f 滿足Inv(s)約束。

定義10(時間自動機的語義) (L，lo，F(xiàn)，I，O，X，E，Inv)的語義定義為一個標記遷移系統(tǒng)(S，So，→)，其中，S ?L ×Rc是一個格局，→?S ×(I ∪O ∪{τ}∪Rc)× S 是一個遷移關系，表示如下:

上述遷移關系定義了兩種情況:

(1)系統(tǒng)仍處于相同狀態(tài)但時間發(fā)生了推移;

(2)系統(tǒng)立即遷移到另一個狀態(tài)并執(zhí)行了一個動作［13］。

多個并發(fā)的時間自動機TA1，…，TAn 可構(gòu)成一個時間自動機網(wǎng)絡 TBAN = (X，TA1‖…‖TAn)，該網(wǎng)絡中的多個自動機之間通過共享時鐘變量X 進行同步。

定義11(時間遷移系統(tǒng))。假設一個時間自動機網(wǎng)絡(X，TA1‖…‖TAn)是由n 個并發(fā)的時間自動機TA1，…，TAn，組成的。它的時間遷移系統(tǒng)被表示為一個三元組(Δ，ρ0，→)，其中，Δ ?(S1× …× Sn)× Rc是一個狀態(tài)集合，ρ0=)是一個初始狀態(tài)，→?Δ ×(I ∪O ∪{τ}∪Rc)× Δ 是一個遷移關系，表示如下:

上述遷移關系定義了三種情況:(1)系統(tǒng)仍處于相同狀態(tài)但時間發(fā)生了推移;(2)系統(tǒng)遷移到另一個狀態(tài)并執(zhí)行了一個內(nèi)部動作;(3)系統(tǒng)遷移到另一個狀態(tài)，并且兩個時間自動機之間執(zhí)行了一個同步動作。

時間自動機上的動作集合對應著Web 服務接口上的端口集合，輸入端口p 對應輸入動作p?，而輸出端口r 對應著輸出動作r!。對于同一類型的端口p，如果存在動作p?和p!，那么(p?，p!)表示這兩個動作可進行同步通信。

對于Web 服務接口的時間約束，主要關注兩個方面:調(diào)用操作(通過一個端口接收或發(fā)送消息)和傳送消息的時間約束。

例如，一個調(diào)用操作的時間相關行為，即先在時間點t1接收一條消息m1，然后在t2時刻發(fā)送另一條消息m2，該行為可建模為圖2 中所示。

圖2 調(diào)用操作的時間相關行為模型

如果上述調(diào)用操作的時間約束要求不超過10個時間單位，則在該時間約束下的行為可建模如在圖3 中所示。

圖3 時間約束下的調(diào)用操作的時間相關行為模型

當Web 服務s1向s2發(fā)送消息時，也就是s1在時間點t1發(fā)送消息m，然后s2在t2時刻接收該消息，這種行為可被建模為圖4 所示。

圖4 發(fā)送消息下的時間相關行為模型

如果發(fā)送消息的時間約束是要求不超過5 個時間單位，那么該行為可建模如在圖5 所示。

圖5 時間約束下的發(fā)送消息時間相關行為模型

4 基于UPPAAL 的模擬和驗證

為了模擬服務組合中的時間行為，本文先將Web 服務接口轉(zhuǎn)化為時間自動機，然后利用模型檢測工具UPPAAL 來模擬和驗證時間自動機網(wǎng)絡的時間屬性［13］。股票分析應用場景中，主要涉及了四個Web 服務:UIS，IMS，SRS 和SBS，將這些服務和各自的時間約束分別轉(zhuǎn)換為時間自動機，如圖6 所示。

圖6 服務UIS，SRS，IMS 和SBS 的時間自動機模型

另外，服務的時間屬性采用UPPAAL 中的時序邏輯公式來表達。這些公式是建立在計算樹邏輯(CTL)的一個子集上，它是由狀態(tài)和路徑公式組成的。狀態(tài)公式用于描述單個狀態(tài)的邏輯性質(zhì)，例如，不變量式t ＜=3;路徑公式用于量化模型的路徑，其語法表示如下:

這些時序邏輯公式用來刻畫服務的具體時間屬性，包括:

(1)服務組合的安全性，即復合服務不出現(xiàn)死鎖，該屬性的時序邏輯公式:

(2)在UIS 發(fā)送一個請求之后，它可能從SBS中獲得的股票投資研究報告:

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

(3)從UIS 發(fā)送請求到SBS 所耗費的時間是不超過10 個時間單位:

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

(4)SBS 必須在8 個時間單位內(nèi)獲得投資者身份的確認結(jié)果:

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

(5)SBS 必須在20 個時間單位內(nèi)獲得研究報告:

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

經(jīng)過模型檢測工具UPPAAL(4.0.13 版本)的自動驗證，上述時間屬性都滿足，分析結(jié)果見圖7。

圖7 股票分析應用場景服務的屬性驗證結(jié)果

5 相關工作

近幾年來，已有一些研究者關注對Web 服務組合如何進行建模和分析。為確保Web 服務組合的正確性，Howard 提出了一種基于BPEL 的形式化語義，將其轉(zhuǎn)化成有限狀態(tài)進程(FSP)模型，并使用LTSA-WS 模型檢查工具對服務組合的行為屬性進行驗證［14］。

Raman 提出了一種基于BPEL 流程定義的Web 服務組合模型，并給出了分析時間屬性的方法。為了刻畫時間行為，他們提出了一種形式化模型稱為Web 服務的時間前移系統(tǒng)。文獻［15］也給出了另一種形式化模型，稱為Web 服務的時間自動機，用于建?；贐PEL 的Web 服務的時間行為。

在文獻［16］中，提出了一種BPEL 流程的形式化模型，稱為μ-BPEL，它能夠支持從μ-BPEL 到時間自動機的轉(zhuǎn)化。

Gregorio 提出了一種時間約束條件下檢查Web 服務正確性的形式化方法，他們采用WSCI語言來描述Web 服務，并將服務轉(zhuǎn)換為時間自動機，然后，利用UPPAAL 工具來模擬和驗證Web 服務組合的時間行為及屬性;然而，該文沒有給出轉(zhuǎn)換為時間自動機的形式化語義。

SENSORIA 項目［2］基于SRML 語言的基礎上，增加了一些新的原語用于刻畫服務執(zhí)行過程中可能發(fā)生的延遲。他們主要關注與時間約束相關方面包括:(1)系統(tǒng)的構(gòu)件處理進程事件以及在其本地狀態(tài)上的計算時間約束;(2)在不同對象之間傳送事件的時間約束;(3)基于SOA 的中間件在執(zhí)行服務的發(fā)現(xiàn)、選擇和綁定上的時間延遲。

6 結(jié)論和未來的工作

在本文中，我們已提出了分析和驗證Web 服務組合的時間屬性的一種形式化框架。該框架引入了時間消息流的概念，建模了Web 服務接口的端口通信歷史。為了描述Web 服務接口的時間約束，本文擴展了標準的WSDL，規(guī)范了時間約束需求。本文采用時間自動機來建模Web 服務的時間行為，多個并發(fā)時間自動機組合成一個時間自動機網(wǎng)絡，并利用模型檢測工具UPPAAL 來驗證服務組合的時間屬性。

在此工作基礎上，將考慮Web 服務編排的時間約束需求，并應用面向服務的實時系統(tǒng)。另外，我們將會考慮采用其他形式化技術(shù)，例如，采用時間Petri 網(wǎng)來刻畫和分析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，F(xiàn)rancesco 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.