基于概率時(shí)間自動(dòng)機(jī)Web服務(wù)質(zhì)量的形式化建模分析

陸 闖,劉淑芬,王曉燕

(吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,長春 130012)

?

基于概率時(shí)間自動(dòng)機(jī)Web服務(wù)質(zhì)量的形式化建模分析

陸 闖,劉淑芬,王曉燕

(吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,長春 130012)

針對拓展的Web服務(wù)體系結(jié)構(gòu),利用概率時(shí)間自動(dòng)機(jī)(probabilistic timed automata,PTA)對Web服務(wù)組合進(jìn)行形式化建模,將Web服務(wù)組合的過程理解為一個(gè)實(shí)時(shí)系統(tǒng)的運(yùn)行過程,進(jìn)而對Web服務(wù)組合的整體服務(wù)質(zhì)量(quality of service,QoS)進(jìn)行定量分析,從而克服了已有Web服務(wù)質(zhì)量研究方式主要集中在對單個(gè)Web服務(wù)分析評(píng)估上的局限性,在整個(gè)分析過程中充分考慮Web服務(wù)組合執(zhí)行過程所具有的隨機(jī)性和不確定性,具有較高的可信度.通過實(shí)驗(yàn)說明了建模分析方法的可行性,并證明了采取相應(yīng)的服務(wù)選擇策略有助于提高Web服務(wù)組合的成功率.

Web服務(wù)組合；概率時(shí)間自動(dòng)機(jī)；定量建模分析；Web服務(wù)質(zhì)量

隨著電子商務(wù)的迅速發(fā)展,Web服務(wù)作為一種新興的Web應(yīng)用模式,受到IT行業(yè)的廣泛關(guān)注.Web服務(wù)是一個(gè)嶄新的分布式計(jì)算模型[1],具有開放的協(xié)議標(biāo)準(zhǔn)和良好的模塊化特性,允許服務(wù)提供者采用不同語言在不同平臺(tái)上開發(fā)松耦合的Web服務(wù),并通過服務(wù)組合支持面向服務(wù)應(yīng)用的集成和開發(fā)[2].在Web服務(wù)組合過程中,需要有大量復(fù)雜的信息在各原子服務(wù)中交互.由于網(wǎng)絡(luò)環(huán)境的開放性和不確定性及Web服務(wù)出現(xiàn)的更新和失效情況,使得Web服務(wù)執(zhí)行過程中有大量的不確定性和隨機(jī)性.因此有必要對Web服務(wù)的服務(wù)質(zhì)量(quality of service,QoS)相關(guān)指標(biāo)進(jìn)行驗(yàn)證.目前,對Web服務(wù)質(zhì)量的研究多數(shù)建立在對單個(gè)原子Web服務(wù)的質(zhì)量評(píng)估上,本文在擴(kuò)展的Web服務(wù)體系結(jié)構(gòu)基礎(chǔ)上,在充分考慮Web服務(wù)組合的隨機(jī)性和不確定性的前提下,重點(diǎn)對多個(gè)Web原子服務(wù)組合的服務(wù)質(zhì)量進(jìn)行建模分析.

概率時(shí)間自動(dòng)機(jī)(probabilistic timed automata,PTA)是一種對具有不確定性和隨機(jī)性的實(shí)時(shí)系統(tǒng)進(jìn)行建模的形式化方法[3].本文采用PTA對Web服務(wù)組合過程進(jìn)行建模,在假設(shè)已有Web服務(wù)在有限代價(jià)花費(fèi)下能滿足用戶最終目的的前提下,利用概率時(shí)間自動(dòng)機(jī)驗(yàn)證工具PRISM形式化分析Web服務(wù)的服務(wù)質(zhì)量.

1 Web服務(wù)QoS模型及相關(guān)指標(biāo)

Web服務(wù)的體系結(jié)構(gòu)由服務(wù)請求者(service requester)、服務(wù)提供者(service provider)和服務(wù)代理(service broker)構(gòu)成.服務(wù)提供者首先將所提供的服務(wù)發(fā)布到服務(wù)代理,當(dāng)服務(wù)請求者請求服務(wù)時(shí),請求者利用服務(wù)代理提供的相關(guān)目錄進(jìn)行搜索,并根據(jù)搜索獲得的相關(guān)信息調(diào)用服務(wù)提供者所提供的服務(wù).可見,在整個(gè)Web服務(wù)執(zhí)行過程中,服務(wù)的發(fā)布和查詢具有重要作用.目前,服務(wù)發(fā)布和查詢使用最廣泛的協(xié)議是UDDI(uiversal description,discovery,integration),但UDDI數(shù)據(jù)結(jié)構(gòu)規(guī)范和API規(guī)范沒有對任何類型的QoS模型提供支持[4],從而導(dǎo)致當(dāng)有多個(gè)可實(shí)現(xiàn)相同功能的Web服務(wù)可被選擇,服務(wù)請求者調(diào)用服務(wù)時(shí),缺乏對Web服務(wù)QoS的形式化指標(biāo)做向?qū)?

文獻(xiàn)[2]在以上Web服務(wù)體系機(jī)構(gòu)的基礎(chǔ)上,提出了一種擴(kuò)展的Web服務(wù)體系結(jié)構(gòu),該結(jié)構(gòu)通過在原有的UDDI數(shù)據(jù)結(jié)構(gòu)中加入服務(wù)的QoS信息(UDDI width QoS),并加入Web服務(wù)質(zhì)量管理器(Web service QoS manager)的結(jié)構(gòu),實(shí)現(xiàn)了對Web原子服務(wù)QoS信息的動(dòng)態(tài)更新(本文中Web原子服務(wù)是指在UDDI中注冊的單個(gè)Web服務(wù)).為了實(shí)現(xiàn)對Web服務(wù)組合服務(wù)質(zhì)量的定量分析,本文沿用文獻(xiàn)[2]中所提出的Web服務(wù)體系結(jié)構(gòu).

目前,對Web服務(wù)QoS的評(píng)估已有多種方法：文獻(xiàn)[2]通過單個(gè)Web原子服務(wù)的相關(guān)指標(biāo)進(jìn)行計(jì)算并保存在擴(kuò)展的UDDI數(shù)據(jù)結(jié)構(gòu)中,對多個(gè)正(負(fù))指標(biāo)的歸一并加權(quán)得到用戶對相應(yīng)Web服務(wù)的滿意程度；文獻(xiàn)[5]以服務(wù)請求者的歷史經(jīng)驗(yàn)為基礎(chǔ),根據(jù)消費(fèi)者之間相似度及服務(wù)之間的相似度,對消費(fèi)者未使用的Web服務(wù)QoS進(jìn)行了預(yù)測；文獻(xiàn)[6]基于時(shí)間自動(dòng)機(jī)對Web服務(wù)進(jìn)行研究；文獻(xiàn)[7]在CCS的基礎(chǔ)上為進(jìn)程動(dòng)作和狀態(tài)擴(kuò)展價(jià)格函數(shù)對Web服務(wù)組合的成本進(jìn)行了分析.本文在擴(kuò)展的Web服務(wù)模型基礎(chǔ)上對Web服務(wù)組合的服務(wù)質(zhì)量進(jìn)行定量分析.

為討論方便,本文沿用文獻(xiàn)[2]中對相關(guān)Web服務(wù)指標(biāo)的定義,在建模分析中僅考慮特定的幾個(gè)Web服務(wù)QoS指標(biāo).下面對單個(gè)Web服務(wù)的相關(guān)性能指標(biāo)進(jìn)行簡要介紹.

1)執(zhí)行代價(jià)：服務(wù)ws的執(zhí)行代價(jià)記為Cost(ws),該執(zhí)行代價(jià)由服務(wù)供應(yīng)商提供,并且為一個(gè)定值.

2)響應(yīng)時(shí)間：從Web服務(wù)ws接收到服務(wù)請求(即獲得相應(yīng)的服務(wù)接口輸入?yún)?shù)),到輸出服務(wù)計(jì)算結(jié)果的時(shí)間,記為T(ws).

3)可靠性：可靠性反映了一個(gè)Web服務(wù)ws的失效率,記為A(ws),其取值越大說明當(dāng)前服務(wù)的失效率越低,則調(diào)用服務(wù)成功的可能性越大.

4)負(fù)載：Web服務(wù)的負(fù)載反映了服務(wù)的實(shí)時(shí)利用率,即單位時(shí)間內(nèi)到達(dá)請求的數(shù)量α與單位時(shí)間內(nèi)所處理的請求數(shù)量β的比值,記為L(ws)=α/β,其值越大表明服務(wù)質(zhì)量越差.

將上述服務(wù)指標(biāo)分為正指標(biāo)(可靠性)和負(fù)指標(biāo)(執(zhí)行代價(jià)、響應(yīng)時(shí)間和負(fù)載).正(負(fù))指標(biāo)表明響應(yīng)指標(biāo)值越大,則響應(yīng)Web服務(wù)質(zhì)量越好(差).本文假設(shè)這些原子Web服務(wù)QoS指標(biāo)評(píng)估值的期望和方差在擴(kuò)展的UDDI中可查詢,并在此基礎(chǔ)上對整個(gè)Web服務(wù)組合的相應(yīng)QoS指標(biāo)進(jìn)行定量分析.

2 概率時(shí)間自動(dòng)機(jī)

2.1時(shí)鐘和時(shí)間概率系統(tǒng)

設(shè)時(shí)鐘x表示記錄時(shí)間的非負(fù)實(shí)數(shù)變量[8],用X表示時(shí)鐘x的有限集合.時(shí)鐘賦值v(clock valuation)被定義為映射：X→≥0,其中≥0表示非負(fù)實(shí)數(shù)的集合.對于任意的時(shí)鐘賦值v和t∈，t≥0,用v+t表示對所有的x∈X有v(x)+t,用v[X∶=0]表示將所有的x∈X復(fù)位為0.

在X上的時(shí)間約束記為CC(X),語法形式定義為

2.2概率時(shí)間自動(dòng)機(jī)模型

概率時(shí)間自動(dòng)機(jī)為具有不確定性和隨機(jī)性的實(shí)時(shí)系統(tǒng),提供了一種形式化的建模方法.在PTA的定義中會(huì)用到時(shí)間概率系統(tǒng)的概念[3],本文沿用文獻(xiàn)[3]和文獻(xiàn)[8]中的相關(guān)定義,對PTA模型進(jìn)行說明.

定義1概率時(shí)間自動(dòng)機(jī)是一個(gè)八元組(L,l,X,act,inv,envb,prob,ζ),其中：L表示一個(gè)位置(locations)的有限集合,l∈L表示初始位置；X表示一個(gè)有限的時(shí)鐘集合；act表示一個(gè)有限的動(dòng)作(actions)集合；inv表示映射：L→CC(X)為一個(gè)狀態(tài)和一個(gè)不變時(shí)鐘約束的映射關(guān)系;envb表示映射：L×act→CC(X),在位置上執(zhí)行動(dòng)作act需要滿足的誘發(fā)條件；prob表示映射：L×act→dist(2x×L),是一個(gè)狀態(tài)轉(zhuǎn)換函數(shù),用來關(guān)聯(lián)每個(gè)狀態(tài)和在2x×L上離散概率分布的確定非空集合,dist(2x×L)即為在2x×L上的一個(gè)離散概率分布；ζ表示映射：L→2AP,是一個(gè)標(biāo)簽函數(shù),用于關(guān)聯(lián)L中的位置l和使得l有效的所有原子命題集合,其中AP為一個(gè)原子命題集合.

2)對于任何s=(l,v)∈S和a∈act,有遷移step(s,a)=γ滿足如下兩個(gè)條件之一：

圖1 基于PTA對網(wǎng)絡(luò)協(xié)議進(jìn)行建模的簡單示例Fig.1 A simple example for modelingnetwork protocol based on PTA

γ(l′,v′)=∑{prob(l,a)(T,l′)|T≥2x∧v′=v[X∶=0];

3)對于任意的(l,v)∈S,lab(l,v)=ζ(l).

可用概率時(shí)間自動(dòng)機(jī)形式化地描述一個(gè)網(wǎng)絡(luò)協(xié)議,如圖1所示.

2.3PTA的性質(zhì)描述

采用PTCTL描述PTA的性質(zhì).文獻(xiàn)[3,8]中已經(jīng)對PTA的性質(zhì)描述進(jìn)行了說明,主要包括概率量詞P～λ[φ]和費(fèi)用量詞R～[ψ],下面進(jìn)行簡要說明：～∈{≤,≥,<,>}；P～λ[-],P～λ[-]是量詞；φ和ψ是路徑公式.

對于圖1中的PTA,下面是兩個(gè)簡單的性質(zhì)描述例子：

1)P<0.9[F<20sec sendn]表示在20 s內(nèi)發(fā)送n條message的概率小于0.9；

2)R<20pic time[end]表示該協(xié)議從啟動(dòng)到結(jié)束的時(shí)間在20 ms內(nèi).

從而基于概率時(shí)間自動(dòng)機(jī)的性質(zhì)分析問題,即轉(zhuǎn)化成了PTA的一個(gè)概率量詞和費(fèi)用量詞是否被滿足的問題.

3 Web服務(wù)組合PTA模型的建立

本文考慮的Web組合屬于靜態(tài)Web組合,即在預(yù)定義流程的基礎(chǔ)上對Web組合的服務(wù)質(zhì)量進(jìn)行建模分析.靜態(tài)Web組合的預(yù)定義流程一般包含串行、并行、選擇和循環(huán)4種結(jié)構(gòu).文獻(xiàn)[9]通過分解選擇路徑和概率展開循環(huán)路徑,將復(fù)雜的預(yù)定義流程圖轉(zhuǎn)換成一個(gè)只有并行和串行兩種結(jié)構(gòu)的DAG圖.因此,本文所提到的Web服務(wù)組合預(yù)定義流程中只包含串行和并行兩種結(jié)構(gòu).

圖2 Web服務(wù)組合預(yù)定義流程示例Fig.2 An example for predefined workflowof Web service composition

圖2為一個(gè)簡單的Web服務(wù)組合預(yù)定義流程示例,其中的每個(gè)任務(wù)表示一個(gè)預(yù)定義流程中的抽象任務(wù),并且任務(wù)1、任務(wù)2和任務(wù)4之間是串行關(guān)系,任務(wù)3_1、任務(wù)3_2和任務(wù)3_3之間是并行關(guān)系.為方便說明Web服務(wù)組合PTA模型的建立過程,給出如下定義.

定義2一個(gè)任務(wù)task的備選服務(wù)集合定義為一個(gè)有限的集合backup(task)={wsi|wsi可實(shí)現(xiàn)task所定義的功能,1≤i≤n}.

定義3一個(gè)原子服務(wù)wsi的最小等待時(shí)間定義為從服務(wù)wsi接收到服務(wù)請求再到輸出結(jié)果的最短延時(shí),記為wait_min(wsi),該變量說明服務(wù)wsi從接收到服務(wù)請求后,最少需要wait_min(wsi)的時(shí)間才能判斷服務(wù)wsi是否執(zhí)行成功.一個(gè)原子服務(wù)wsi的最大等待時(shí)間定義為從服務(wù)wsi接收到服務(wù)請求再到輸出結(jié)果的最長延時(shí),記為wait_max(wsi).

服務(wù)wsi的響應(yīng)時(shí)間T(wsi)所服從的概率分布無法確定,但通過UDDI可查詢到wsi的期望相應(yīng)時(shí)間E(T(wsi))及其方差D(T(wsi)).可根據(jù)Chebyshev不等式計(jì)算wait_min(wsi)和wait_max(wsi)：

(1)

(2)

其中ε>0.

圖3 任務(wù)task(i)的PTA模型Fig.3 PTA model of task(i)

在上述討論的基礎(chǔ)上,本文對Web服務(wù)組合預(yù)定義流程中的抽象任務(wù)進(jìn)行PTA建模.不失一般性,假設(shè)對于任務(wù)task(i)的備選服務(wù)集合backup(task(i))={ws1,ws2,…,wsn},則task(i)執(zhí)行過程所對應(yīng)的PTA模型如圖3所示,其中：任務(wù)task(i)對于每個(gè)備選服務(wù)wsi的選擇是不確定的；P(wsi_success)表示任務(wù)執(zhí)行的成功概率,是一個(gè)隨機(jī)變量.實(shí)際執(zhí)行中,P(wsi_success)的取值不僅與服務(wù)wsi本身執(zhí)行的質(zhì)量有關(guān),也與當(dāng)前的負(fù)載有關(guān).本文將P(wsi_success)的取值設(shè)定為在UDDI中的查詢結(jié)果,即A(ws).

4 應(yīng)用實(shí)例

為了說明使用PTA對Web服務(wù)組合QoS進(jìn)行分析的可行性,本文對如圖4所示定義的一個(gè)簡單Web服務(wù)組合進(jìn)行分析.首先在預(yù)定義任務(wù)隨機(jī)選擇備選服務(wù)的情況下對整個(gè)服務(wù)組合過程進(jìn)行定量分析,然后提出一種備選服務(wù)的選擇策略,并在該策略的基礎(chǔ)上得出相應(yīng)的分析結(jié)果,再將兩次分析結(jié)果加以對比,以證明文獻(xiàn)[2]所提出的Web服務(wù)組合方法有助于提高Web服務(wù)組合的整體成功率.

4.1實(shí)驗(yàn)數(shù)據(jù)設(shè)定

圖4 一個(gè)簡單Web服務(wù)組合流程Fig.4 A simple workflow of Web service composition

為了實(shí)現(xiàn)對圖4中的預(yù)定義組合流程進(jìn)行分析,做如下假設(shè)：

1)預(yù)定義流程與備選服務(wù)對應(yīng)關(guān)系列于表1；

2)備選服務(wù)相應(yīng)指標(biāo)在擴(kuò)展UDDI中的查詢結(jié)果列于表2,其中相應(yīng)時(shí)間的查詢值為二元組(E(T(wsi)),D(T(wsi))).

表1 備選服務(wù)集合Table 1 Sets of alternative services

表2 備選服務(wù)相關(guān)QoS指標(biāo)Table 2 QoS metrics of alternative service

4.2實(shí)驗(yàn)分析

根據(jù)以上假設(shè)數(shù)據(jù),首先在預(yù)定義任務(wù)隨機(jī)選擇備選服務(wù)的前提下對圖4所定義的Web服務(wù)組合流程進(jìn)行定量分析.圖5為圖4中任務(wù)1所對應(yīng)的PTA模型,其他預(yù)定義任務(wù)所對應(yīng)的PTA模型與其類似.本文使用模型檢測工具PRISM對服務(wù)組合的最小(期望)成功概率進(jìn)行分析:

{1-Pmax= ?[F“fail”]}=0.398 43.

圖5 Task1的PTA模型Fig.5 PTA model of task1

實(shí)驗(yàn)中對于wait_min(wsi)和wait_max(wsi)的計(jì)算,本文設(shè)可變參數(shù)ε=3,根據(jù)Chebyshev定理可知在實(shí)際運(yùn)行中服務(wù)wsi的響應(yīng)時(shí)間在wait_min(wsi)和wait_max(wsi)之間的可能性高于0.89,具有相當(dāng)高的可信度.

在以上實(shí)驗(yàn)的基礎(chǔ)上,本文對圖5所示的概率時(shí)間自動(dòng)機(jī)應(yīng)用文獻(xiàn)[2]所提出的備選服務(wù)選擇策略：性能越好的備選服務(wù)被選擇的概率越大.

定義4一個(gè)備選服務(wù)ws1∈backup(task)的選擇概率是指在任務(wù)組合流程執(zhí)行到任務(wù)task時(shí),服務(wù)wsi被選中實(shí)現(xiàn)task所定義任務(wù)的概率,記為P(task,wsi).

P(task,wsi)的設(shè)定方法遵循性能越好的服務(wù)則給予越大的選擇概率,計(jì)算方法如下：設(shè)task(i)的備選服務(wù)集合為{ws1,ws2,…,wsn},則任務(wù)wsi≥backup(task(i))被選中的概率為

(3)

其中,quality(wsj)是服務(wù)wsj的綜合性能指標(biāo),計(jì)算方法為

(4)

式中:Qt(-)/(+)(wsj)是服務(wù)wsj的正(負(fù))指標(biāo)t(t≥{cost(wsj),T(wsj),A(wsj),L(wsj)})的期望及方差的歸一值;ωt是單方面指標(biāo)在綜合指標(biāo)中所占的權(quán)重;m表示Qt(-)/(+)(wsj)綜合了服務(wù)wsj的m個(gè)單方面指標(biāo)值,本文中m=4.

圖6為在對圖5的PTA模型應(yīng)用文獻(xiàn)[2]中所提出的備選服務(wù)選擇策略后任務(wù)1的執(zhí)行過程.由圖6可見,在相應(yīng)的策略下,將PTA的不確定性行為轉(zhuǎn)化成概率選擇事件,即預(yù)定義任務(wù)對備選服務(wù)的選擇由完全隨機(jī)性行為變?yōu)榘凑障鄳?yīng)概率P(task,wsj)進(jìn)行選擇.

圖6 應(yīng)用策略的任務(wù)執(zhí)行模型Fig.6 Model of task executing under adversary

本文假設(shè)用戶更注重服務(wù)組合的總體響應(yīng)時(shí)間和組合成功率,因此在對備選服務(wù)wsi綜合指標(biāo)quality(wsi)計(jì)算過程中,將各指標(biāo)對應(yīng)的權(quán)值系數(shù)設(shè)置列于表3.

表3 相關(guān)QoS指標(biāo)權(quán)重系數(shù)Table 3 Weight coefficient of QoS metrics

圖7 組合執(zhí)行過程中的失敗概率比較Fig.7 Failure probability during the executionof combination

在文獻(xiàn)[2]的策略下,對組合最小(期望)成功概率進(jìn)行分析可得：{1-Pmax=?[F “fail”]}=0.565 71.進(jìn)一步對整個(gè)Web服務(wù)執(zhí)行過程中服務(wù)失敗的概率進(jìn)行分析,表明在文獻(xiàn)[2]中的備選服務(wù)選擇策略下,整個(gè)Web服務(wù)組合在執(zhí)行過程中的任意時(shí)刻出現(xiàn)組合失敗的概率都低于不使用任何策略的Web服務(wù)組合.圖7為圖4所定義的Web服務(wù)組合流程分別在文獻(xiàn)[2]中的備選服務(wù)選擇策略下和無策略下執(zhí)行過程中出現(xiàn)組合失敗的概率.由圖7可見,按照文獻(xiàn)[2]所提出的備選服務(wù)選擇策略進(jìn)行Web服務(wù)組合,可有效提高整個(gè)服務(wù)組合的成功率.

綜上所述,本文通過使用PTA對靜態(tài)Web服務(wù)組合進(jìn)行了形式化建模,并在此基礎(chǔ)上對Web服務(wù)組合的相關(guān)性能指標(biāo)進(jìn)行了定量分析.在分析過程中充分考慮了Web服務(wù)組合中存在的隨機(jī)性和不確定性,具有較高的可信度,對于評(píng)估一個(gè)Web服務(wù)的綜合質(zhì)量具有指導(dǎo)作用.實(shí)驗(yàn)結(jié)果表明,在服務(wù)組合過程中應(yīng)用文獻(xiàn)[2]所提出的策略可提高整個(gè)服務(wù)組合的成功率.

[1] 岳昆,王曉玲,周傲英.Web服務(wù)核心支撐技術(shù):研究綜述 [J].軟件學(xué)報(bào),2004,15(3):428-442.(YUE Kun,WANG Xiaoling,ZHOU Aoying.Underlying Techniques for Web Services:A Survey [J].Journal of Software,2004,15(3):428-442.)

[2] 范小芹,蔣昌俊,王俊麗,等.隨機(jī)QoS感知的可靠Web服務(wù)組合 [J].軟件學(xué)報(bào),2009,20(3):546-556.(FAN Xiaoqin,JIANG Changjun,WANG Junli,et al.Random-QoS-Aware Reliable Web Service Composition [J].Journal of Software,2009,20(3):546-556.)

[3] Norman G,Parker D,Sproston J.Model Checking for Probabilistic Timed Automata [J].Formal Methods in System Design,2013,43(2):164-190.

[4] 郭得科,任彥,陳洪輝,等.一種QoS有保障的Web服務(wù)分布式發(fā)現(xiàn)模型 [J].軟件學(xué)報(bào),2006,17(11):2324-2334.(GUO Deke,REN Yan,CHEN Honghui,et al.A QoS-Guaranteed and Distributed Model for Web Service Discovery [J].Journal of Software,2006,17(11):2324-2334.)

[5] 邵凌霜,周立,趙俊峰,等.一種Web Service的服務(wù)質(zhì)量預(yù)測方法 [J].軟件學(xué)報(bào),2009,20(8):2062-2073.(SHAO Lingshuang,ZHOU Li,ZHAO Junfeng,et al.Web Service QoS Prediction Approach [J].Journal of Software,2009,20(8):2062-2073.)

[6] 駱翔宇,軒愛成,沙宗魯.基于時(shí)間自動(dòng)機(jī)的Web服務(wù)模型檢測 [J].計(jì)算機(jī)科學(xué),2010,37(8):139-142.(LUO Xiangyu,XUAN Aicheng,SHA Zonglu.Model Checking Web Services Based on Timed Automata [J].Computer Science,2010,37(8):139-142.)

[7] 肖芳雄,黃志球,曹子寧,等.基于價(jià)格進(jìn)程代數(shù)的Web服務(wù)組合描述和成本分析 [J].計(jì)算機(jī)研究與發(fā)展,2009,46(5):832-840.(XIAO Fangxiong,HUANG Zhiqiu,CAO Zining,et al.Describing and Cost Analyzing of Web Services Composition Using PPA [J].Journal of Computer Research and Development,2009,46(5):832-840.)

[8] 張君華,黃志球,曹子寧.模型檢測基于概率時(shí)間自動(dòng)機(jī)的反例產(chǎn)生研究 [J].計(jì)算機(jī)研究與發(fā)展,2008,45(10):1638-1645.(ZHANG Junhua,HUANG Zhiqiu,CAO Zining.Counterexample Generation for Probabilistic Timed Automata Model Checking [J].Journal of Computer Research and Development,2008,45(10):1638-1645.)

[9] Ardagna D,Pernici B.Adaptive Service Composition in Flexible Processes [J].IEEE Trans on Software Engineering,2007,33(6):369-384.

(責(zé)任編輯：韓 嘯)

FormalModelingAnalysisofWebQoSBasedonPTA

LU Chuang,LIU Shufen,WANG Xiaoyan

(CollegeofComputerScienceandTechnology,JilinUniversity,Changchun130012,China)

In view of the extended Web service architecture,we formally modeled the Web service composition with probabilistic timed automata (PTA).The process of Web service composition was understood as a real-time system operation process.We then overcame the limitation of existing research approach of Web service quality which focused the service quality on a single Web service,by quantitatively analyze the quality of Web service composition on the basis of the model we built before.The stochastic and nondeterministic characteristics in the execution of Web service composition were fully taken into account in the whole analysis so as to make the result credible.Finally,an example was given to illustrate the feasibility of the modeling analysis method,proving that the corresponding service selection strategy can improve the success probability of Web service composition.

Web service composition;probabilistic timed automata;quantitative modeling analysis;quality of Web service

10.13413/j.cnki.jdxblxb.2015.03.34

2014-03-23.

陸 闖(1990—),男,漢族,碩士研究生,從事軟件模型檢測技術(shù)和軟件工程的研究,E-mail:jlu_chuang@163.com.通信作者：劉淑芬(1950—),女,漢族,教授,博士生導(dǎo)師,從事計(jì)算機(jī)支持協(xié)同工作、軟件體系結(jié)構(gòu)、基于模型驅(qū)動(dòng)的軟件編程方法和網(wǎng)絡(luò)管理技術(shù)的研究,E-mail:liusf@mail.jlu.edu.cn.

國家自然科學(xué)基金(批準(zhǔn)號(hào):60973041)、國家高技術(shù)研究發(fā)展計(jì)劃863項(xiàng)目基金(批準(zhǔn)號(hào):2009AA010314)和吉林省科技發(fā)展計(jì)劃項(xiàng)目(批準(zhǔn)號(hào):20115007).

TP311

：A

：1671-5489(2015)03-0531-07