陳志輝 ，吳敏敏

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

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

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

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

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

1 案例研究

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

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

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

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

2 Web 服務(wù)

Web 服務(wù)是一個(gè)自描述的和獨(dú)立的軟件實(shí)體，它利用標(biāo)準(zhǔn)的語言和協(xié)議在互聯(lián)網(wǎng)上進(jìn)行發(fā)布、發(fā)現(xiàn)和調(diào)用［9］。其中一個(gè)關(guān)鍵技術(shù)就是Web服務(wù)描述語言WSDL，將服務(wù)看作為一個(gè)抽象的端口集合。WSDL 還定義了Web 服務(wù)以何種動(dòng)作來傳送數(shù)據(jù)。一個(gè)動(dòng)作就是一個(gè)操作，數(shù)據(jù)由消息來表示。相關(guān)操作的集合稱為一個(gè)端口類型。端口類型就是Web 服務(wù)所提供的操作集合。例如，一個(gè)Web 服務(wù)的WSDL 接口定義如下:

＜definitions…＞

＜portType name ="investorAuthentication" ＞

＜o(jì)peration name="getAuthenti

cation" ＞

＜inputname ="getAuthentica

tionRequest"/ ＞

＜o(jì)utputname ="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 ＞

為了描述時(shí)間約束，本文擴(kuò)展了標(biāo)準(zhǔn)的WSDL的constraint 元素。該元素是刻畫operation 和message 元素中的時(shí)間約束關(guān)系，并且是可選的。如果一個(gè)操作operation 有時(shí)間約束，那么duration 用于規(guī)范從接收一個(gè)input message 到發(fā)送一個(gè)output message 的時(shí)間單元值。

＜o(jì)peration name="getAuthenti

cation" ＞

＜inputname ="getAuthentica

tionRequest"/ ＞

＜o(jì)utputname ="getAuthenti

cationResponse”/)

＜constraint duration=10/)

＜/operation ＞

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

＜message name="getAuthentication" ＞

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

＜constraint transmissionTime ＜=5/ ＞

＜/message ＞

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

2.1 Web 服務(wù)的形式化模型

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

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

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

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

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

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

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

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

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

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

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

由于一個(gè)服務(wù)行為可看作是輸入和輸出端口歷史之間的關(guān)系，則將它定義為一個(gè)函數(shù)B:^I →δ(^O)。

從概念上，兩個(gè)服務(wù)之間進(jìn)行通信可看作是一種服務(wù)組合方式，而且組合之后的這兩個(gè)服務(wù)就成為了一個(gè)服務(wù)，稱為復(fù)合服務(wù)。因而，服務(wù)組合可定義如下:

定義8(服務(wù)組合) 服務(wù)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 時(shí)間約束的Web 服務(wù)接口

為了描述Web 服務(wù)接口的時(shí)間約束，本文擴(kuò)展了標(biāo)準(zhǔn)的WSDL，增加了時(shí)間約束標(biāo)簽。C(I，O)表示W(wǎng)eb 服務(wù)接口〈I，O〉上的一個(gè)時(shí)間約束，要求該服務(wù)的行為應(yīng)該滿足C(I，O)，記作:B | =C(I，O)。

例如，存在一個(gè)Web 服務(wù)有兩個(gè)端口:一個(gè)輸入端口p1 和一個(gè)輸出端口p2 ，它的接口為〈Is，Os〉以及時(shí)間約束C(Is，Os)= 5 。假設(shè)

如果| tp2- tp1|≤C(IS，OS)，那么Bs| =C(Is，Os)。

相應(yīng)地，給定的兩個(gè)服務(wù)s1 和s2，以及時(shí)序約束C1(I1，O1)和C2(I2，O2)，s1 ⊕s2 的行為必須滿足所有的時(shí)間約束，記為Bs1⊕s2| = C1(I1，O1)∧C2(I2，O2)。為了確認(rèn)該服務(wù)組合是否滿足時(shí)序約束的需求，接下來將先建模每個(gè)服務(wù)的時(shí)間行為，再通過模型檢查技術(shù)來驗(yàn)證服務(wù)組合的時(shí)間屬性。

3 時(shí)間自動(dòng)機(jī)

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

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

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

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

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

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

(4)I 是一個(gè)輸入端口集(或輸入動(dòng)作集);

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

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

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

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

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

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

上述遷移關(guān)系定義了兩種情況:

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

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

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

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

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

時(shí)間自動(dòng)機(jī)上的動(dòng)作集合對(duì)應(yīng)著Web 服務(wù)接口上的端口集合，輸入端口p 對(duì)應(yīng)輸入動(dòng)作p?，而輸出端口r 對(duì)應(yīng)著輸出動(dòng)作r!。對(duì)于同一類型的端口p，如果存在動(dòng)作p?和p!，那么(p?，p!)表示這兩個(gè)動(dòng)作可進(jìn)行同步通信。

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

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

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

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

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

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

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

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

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

4 基于UPPAAL 的模擬和驗(yàn)證

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

圖6 服務(wù)UIS，SRS，IMS 和SBS 的時(shí)間自動(dòng)機(jī)模型

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

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

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

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

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

(3)從UIS 發(fā)送請(qǐng)求到SBS 所耗費(fèi)的時(shí)間是不超過10 個(gè)時(shí)間單位:

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

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

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

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

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

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

圖7 股票分析應(yīng)用場景服務(wù)的屬性驗(yàn)證結(jié)果

5 相關(guān)工作

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

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

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

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

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

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

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

在此工作基礎(chǔ)上，將考慮Web 服務(wù)編排的時(shí)間約束需求，并應(yīng)用面向服務(wù)的實(shí)時(shí)系統(tǒng)。另外，我們將會(huì)考慮采用其他形式化技術(shù)，例如，采用時(shí)間Petri 網(wǎng)來刻畫和分析Web 服務(wù)的時(shí)間行為。

［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.