許興旺,駱翔宇,2

(1.華僑大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,福建廈門361021;2.桂林電子科技大學(xué)廣西可信軟件重點(diǎn)實(shí)驗(yàn)室,廣西桂林541004)

基于MAS模型檢測與抽象的Web服務(wù)驗(yàn)證

許興旺1,駱翔宇1,2

(1.華僑大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,福建廈門361021;2.桂林電子科技大學(xué)廣西可信軟件重點(diǎn)實(shí)驗(yàn)室,廣西桂林541004)

Web服務(wù)組合現(xiàn)已成為跨組織業(yè)務(wù)流程集成的關(guān)鍵技術(shù),然而在松耦合開發(fā)模式和開放的互聯(lián)網(wǎng)運(yùn)行環(huán)境下,其正確性、可靠性、安全性等可信性質(zhì)難以得到保證。為解決該問題,提出一種Web服務(wù)組合形式化驗(yàn)證方法,將基于圖狀反例向?qū)У某橄笈c精化方法應(yīng)用于多主體系統(tǒng)(MAS)模型檢測工具(MCTK)中,大幅緩解模型檢測的狀態(tài)爆炸問題,從理論上證明該驗(yàn)證方法的正確性。實(shí)驗(yàn)通過將銀行貸款風(fēng)險(xiǎn)評估系統(tǒng)轉(zhuǎn)換成MCTK描述的MAS,并對比抽象前后的模型檢測代價(jià),結(jié)果顯示,基于抽象的Web服務(wù)驗(yàn)證方法明顯優(yōu)于未采用抽象技術(shù)的驗(yàn)證方法。

Web服務(wù)組合;多主體系統(tǒng);模型檢測;圖狀反例;抽象;精化

1 概述

面向Web服務(wù)的軟件開發(fā)已成為跨組織業(yè)務(wù)流程集成的關(guān)鍵技術(shù)。然而,單一Web服務(wù)功能有限,在多數(shù)情況下不能滿足用戶需求,因此出現(xiàn)將多個Web服務(wù)按某種特定組合集成為一個面向不同需求用戶且有統(tǒng)一接口服務(wù)的技術(shù)。由于服務(wù)及其協(xié)同的動態(tài)性,開放多變的互聯(lián)網(wǎng)運(yùn)行環(huán)境以及松耦合的服務(wù)開發(fā)模式導(dǎo)致開發(fā)和運(yùn)行過程不確定,使得服務(wù)的正確性、可靠性、安全性、可用性、時效性等可信性質(zhì)難以得到保證［1］。

目前,研究者主要應(yīng)用模型檢測［2］的方法來驗(yàn)證服務(wù)組合的上述性質(zhì)。如文獻(xiàn)［3］用模型檢測器SPIN自動分析提取來自BPEL的、擴(kuò)展有限狀態(tài)自

動機(jī)EFA轉(zhuǎn)化的、Promela語言描述的程序的方法,文獻(xiàn)［4］用UPPAAL分析驗(yàn)證WS-CDL和WSBPEL并且自動將其轉(zhuǎn)化為的有序時間狀態(tài)機(jī)的方法,文獻(xiàn)［5］給出利用自主研發(fā)的模型檢測工具WSAT進(jìn)行驗(yàn)證的方法。但上述驗(yàn)證方法均不支持驗(yàn)證服務(wù)組合的時態(tài)認(rèn)知性質(zhì)。為此,文獻(xiàn)［6-7］將Web服務(wù)組合描述成多主體系統(tǒng)(Multi-Agent System,MAS),并用模型檢測器MCMAS驗(yàn)證了其計(jì)算樹邏輯(Computation Tree Logic,CTL)性質(zhì)和認(rèn)知性質(zhì)。文獻(xiàn)［1］將BPEL描述的Web服務(wù)組合流程轉(zhuǎn)換為模型檢測器MCTK的輸入語言描述的多主體系統(tǒng),并驗(yàn)證了Web服務(wù)組合的時態(tài)認(rèn)知性質(zhì)。文獻(xiàn)［9］提出將Web服務(wù)組合轉(zhuǎn)換成MCMAS的輸入語言描述的多主體系統(tǒng),并驗(yàn)證了其時態(tài)認(rèn)知性質(zhì)。文獻(xiàn)［8］把Web服務(wù)分別轉(zhuǎn)換為MCTK描述的多主體系統(tǒng)和MCMAS描述的多主體系統(tǒng),并用這2種工具分別驗(yàn)證時態(tài)認(rèn)知性質(zhì),通過對比驗(yàn)證所花代價(jià)證明了MCTK的性能優(yōu)于MCMAS。

然而,上述方法均未采用優(yōu)化技術(shù)來緩解模型檢測的狀態(tài)爆炸問題。由于Web服務(wù)組合的狀態(tài)空間巨大,因此本文采用能有效緩解狀態(tài)爆炸問題的抽象方法［10］,并基于模型檢測多主體系統(tǒng)驗(yàn)證Web服務(wù)組合的CTL性質(zhì)和時態(tài)認(rèn)知性質(zhì)。

2 基本概念

其中,Δi表示各Δ在i上的分量;Δ代表S,R或I。對于全局狀態(tài)s和s′,定義s～is′?si=s′i,容易證明這是一個等價(jià)關(guān)系。給定一個抽象函數(shù)h和上述定義的Kripke結(jié)構(gòu)M,M關(guān)于h的抽象模型定義為,滿足:

將所需驗(yàn)證的邏輯統(tǒng)一用CTLK(Computation Tree of Logic and Knowledge)表示,其意義語法和語義可在文獻(xiàn)［13］中查詢,為便于本文有關(guān)定理證明,僅給出個體知識Kiφ,普遍知識EGφ和公共知識CGφ的語義,其中,φ是任意ECTLK公式。

如果將抽象函數(shù)看成一個模擬函數(shù),從抽象模型的定義來看,抽象模型和原始模型的關(guān)系滿足以上偏序模擬關(guān)系的每個條件,從而可以得出抽象函數(shù)就是抽象模型和原始模型間的偏序模擬關(guān)系。

定理1設(shè),h是一個抽象函數(shù),則對于任意ACTLK公式φ,有。

3 時態(tài)認(rèn)知邏輯的圖狀反例

為給出圖狀反例,考慮一個簡單的認(rèn)知邏輯公式Kiφ,其中,φ是一個純時態(tài)公式。從個體知識的定義可知(M,s)|≠Kiφ??s′(s～is′∧(M,s′)|=φ)。因此,存在一個主體i在狀態(tài)s下的可能世界s′(如果s～is′成立,s′是主體i在s下的可能到達(dá)世

界),s′是純時態(tài)公式?φ的證據(jù)。在已有文獻(xiàn)中,純時態(tài)公式的反例和證據(jù)都是一個線性路徑,因此,這條證據(jù)也是一條線性路徑。在模型檢測中,對于任一公式θ,有M|=Kiφ??s0(I(s0)→(M,s′)|=φ)。

圖1是Kiφ的一個圖狀反例示意圖。其中,φ是純時態(tài)公式;圓圈表示狀態(tài);標(biāo)記i的虛線表明對于主體i來說,虛線兩端的狀態(tài)互為對方的認(rèn)知可達(dá)狀態(tài);s0和s0′都是初始狀態(tài);箭頭表示狀態(tài)遷移;省略號表示一條由若干狀態(tài)構(gòu)成的線性路徑(可以是空的狀態(tài)序列)。這個反例由認(rèn)知和時態(tài)路徑兩部分組成,最外層的時態(tài)路徑部分為s0′→…→s1→…,認(rèn)知部分由狀態(tài)s0,s1以及它們之間的虛線構(gòu)成,把這種反例稱為時態(tài)認(rèn)知邏輯公式的圖狀反例。

圖1 Kiφ的圖狀反例

定義時態(tài)認(rèn)知邏輯公式的反例的圖狀結(jié)構(gòu)為D=(EP,linki(s,s′),T),其中:

(1)T反例最外層的一條時態(tài)路徑稱為反例的時態(tài)部分,它或者是一條有限的路徑,或者是一條尾端帶環(huán)的無限路徑。

(2)EP=空集|圖狀反例,稱為認(rèn)知部分。

(3)linki(s,s′)表示認(rèn)知部分(如果不為空)最外層的一個狀態(tài)s和T中的一個狀態(tài)s′具有認(rèn)知可達(dá)關(guān)系s～is′,其中,i是出現(xiàn)在公式最外層的主體。

如果公式是純時態(tài)公式,則EP為空,反例為一條時態(tài)路徑,即說明純時態(tài)公式的反例也是圖狀的反例,因?yàn)榧儠r態(tài)公式也是時態(tài)認(rèn)知公式。

4 圖狀反例向?qū)У某橄笈c精化

由定理1的證明和上文討論得到定理2。由于篇幅所限,證明過程省略。

定理2如果狀態(tài)空間相同的模型與M有以下近似關(guān)系,則對于任意ACTLK公式φ,有。

4.1 初始抽象系統(tǒng)的生成

在實(shí)際抽象中,計(jì)算抽象系統(tǒng)的近似系統(tǒng)(簡稱近似抽象系統(tǒng)),從定理1和定理2可以推知,如果一個ACTLK公式在近似抽象系統(tǒng)中成立,則其一定在原始系統(tǒng)中成立。然而,這個斷言的否命題和逆命題卻不成立,因此,在實(shí)際抽象中,把這個近似抽象系統(tǒng)叫做初始抽象系統(tǒng),在后續(xù)中還將根據(jù)實(shí)際情況對其進(jìn)行精化。

采用文獻(xiàn)［11］中提及的近似技術(shù),文獻(xiàn)［11］證明了該近似技術(shù)能保證近似系統(tǒng)的條件,即如果是通過這種近似技術(shù)得到的模型,是原始模型的抽象模型,則有,從而有。

將初始狀態(tài)集合I、遷移關(guān)系集合R看成是定義在系統(tǒng)變量集合V={vi|1≤i≤n}上的n元謂詞。設(shè)h為抽象函數(shù),其定義為:

轉(zhuǎn)換函數(shù)A將V上的任意n元謂詞P轉(zhuǎn)換成上的n元謂詞函數(shù)。其中,是近似抽象系統(tǒng)的系統(tǒng)變量集合,只不過其定義域?yàn)?。轉(zhuǎn)換函數(shù)定義如下:

(1)如果P是原子謂詞,則:

(2)如果P=P1∧P2,則A(P)=A(P1)∧A(P2);

(3)如果P=P1∨P2,則A(P)=A(P1)∨A(P2);

(4)如果P=?vP′,則A(P)=?v^A(P′);

(5)如果P=?vP′,則A(P)=?v^A(P′)。

在實(shí)際中,抽象是針對自主研發(fā)的多主體系統(tǒng)模型檢測工具M(jìn)CTK的輸入語言的抽象。MCTK在對輸入語言描述的系統(tǒng)作模型檢測時,以二元決策圖(Binary Decision Diagram,BDD)表示其從輸入文件中抽取的初始狀態(tài)集合和遷移關(guān)系集合。把這2個集合分別用?和?表示,利用BDD運(yùn)算A,計(jì)算出抽象模型狀態(tài)空間、A(?)和A(?),即得到一個近似抽象系統(tǒng)。因?yàn)镸CTK是符號化模型檢測器,所以使用BDD作上述運(yùn)算。

根據(jù)文獻(xiàn)［11］對這種初始抽象系統(tǒng)生成方法做了一些改進(jìn),具體如下:因?yàn)檩斎胝Z言的程序中包含對系統(tǒng)遷移條件的描述,以及待驗(yàn)證性質(zhì)的描述,并且遷移條件由原子命題的布爾運(yùn)算構(gòu)成,驗(yàn)證的性質(zhì)在布爾運(yùn)算基礎(chǔ)上又加了時態(tài)算子和認(rèn)知算子,所以,從輸入語言程序中可以抽取出一個原子命題集合。令A(yù)表示這個集合。將A作以下劃分,以FC=×jFCj表示這個劃分,函數(shù)F:A→FC表示劃分函數(shù)。劃分原則為:?θ1,θ2∈A(F(θ1)=F(θ2)?var(θ1)∩var(θ2)≠Φ),其中,var(θ)表示出現(xiàn)在原子命題θ中的變量集合。

4.2 圖狀反例向?qū)У木?/p>

如上文敘述,在初始抽象系統(tǒng)中不成立的性質(zhì)在原始系統(tǒng)中不一定不成立。這種情況下模型檢測給出的反例稱為偽反例。對于純時態(tài)邏輯公式,其原因及消除偽反例的方法在文獻(xiàn)［11］中已經(jīng)敘述。

對于時態(tài)認(rèn)知公式,通過圖2舉例說明。假設(shè)待驗(yàn)證的公式是Ki(y＜2),抽象后,待驗(yàn)證的公式為。圖2中原始系統(tǒng)的可達(dá)狀態(tài)只有圖2中所示的3個初始狀態(tài)。各圖形符號的含義與圖1中相同,狀態(tài)中標(biāo)明的系統(tǒng)變量在狀態(tài)中取值。原始系統(tǒng)左邊2個狀態(tài)被抽象為初始抽象系統(tǒng)左邊的狀態(tài)。

圖2 初始抽象實(shí)例

因?yàn)閷τ跁r態(tài)部分的精化與文獻(xiàn)［11］中的精化相同,通過簡單推理可以證明其可以把上文中前2個原因消除,所以本文的精化只考慮第(3)個原因。消除這個原因叫做消除偽認(rèn)知,與偽反例時態(tài)部分相對應(yīng)。

消除偽反例的前提是確定反例就是偽反例,即識別偽反例。純時態(tài)公式的偽反例的識別及消除在文獻(xiàn)［11］中已有詳述,并且圖狀偽反例時態(tài)部分的識別和消除與其基本一致,因此本文僅考慮消除偽認(rèn)識。

在下文識別偽反例算法splitCounterexample中,將splitSequence表示識別時態(tài)部分,如果反例不是偽反例,則splitSequence返回一個反例,否則返回一個失敗狀態(tài)集,返回結(jié)果可參見文獻(xiàn)［11］。

算法1splitCounterexample Algorithm

其中第19行的K(S,i)表示主體i在狀態(tài)集合S中所有可能世界的集合,如果時態(tài)部分是偽時態(tài),則第2行返回一個失敗狀態(tài)集,如果認(rèn)知部分是偽認(rèn)知,則第20行返回2個失敗狀態(tài)集,否則返回一個圖狀反例。下文是識別認(rèn)知部分反例的算法。

算法2splitEP Algorithm

算法3PolyRefineEpistemic Algorithm

5 Web服務(wù)組合的驗(yàn)證

在現(xiàn)有基于多主體系統(tǒng)模型檢測來驗(yàn)證Web服務(wù)組合的方法中,通常是通過某種手段把Web服務(wù)組合轉(zhuǎn)化為一種多主體系統(tǒng)的形式化模型,然后將這種模型通過模型檢測器的輸入語言輸入到模型

檢測器中,并在輸入文件中人工加入需要驗(yàn)證的Web服務(wù)組合的性質(zhì),最后執(zhí)行模型檢測,模型檢測返回的驗(yàn)證結(jié)果即為驗(yàn)證服務(wù)組合的結(jié)果。

文獻(xiàn)［1,8］分析了BPEL所描述的Web服務(wù)組合業(yè)務(wù)流程和WSDL所描述的各服務(wù)接口,把BPEL語法結(jié)構(gòu)轉(zhuǎn)換成一種中間結(jié)構(gòu)遷移七元組,然后將這種遷移七元組轉(zhuǎn)換成多主體系統(tǒng)的Kripke結(jié)構(gòu),最后使用MCTK驗(yàn)證這個多主體系統(tǒng)。

采用上述基于轉(zhuǎn)換的建模方法,結(jié)合本文提出的圖狀反例向?qū)У某橄笈c精化,構(gòu)成本文驗(yàn)證方法。通過改進(jìn)MCTK,使其能夠生成本文的圖狀反例,并能夠運(yùn)行下文中的機(jī)械算法。算法中包含的Web服務(wù)組合到多主體系統(tǒng)的轉(zhuǎn)換算法已在文獻(xiàn)［1,8］中實(shí)現(xiàn),并且由4.1節(jié)可以容易得出抽象算法,所以不再詳述這些算法,用transAlgorithm和Abstract Algorithm分別表示轉(zhuǎn)換和抽象算法,RefineAlgorithm表示將時態(tài)部分精化算法和算法3整合后得到的算法。假設(shè)不論splitCounterexample返回幾個失敗集,返回結(jié)果都將輸入RefineAlgorithm由其進(jìn)行精化。由于算法是機(jī)械的,且篇幅有限,因此用自然語言描述該驗(yàn)證算法。

算法4Verification Algorithm

Verification(Composition)//Composition是待驗(yàn)證Web服務(wù)組合

(1)運(yùn)行transAlgorithm(Composition)將Composition轉(zhuǎn)化為SMV描述的多主體系統(tǒng)MAS并在其中加入待驗(yàn)證的性質(zhì)φ;

(2)MCTK讀入多主體系統(tǒng)描述模型,運(yùn)行Abstract Algorithm(MAS)獲得初始抽象系統(tǒng)MASabs;

(3)運(yùn)行模型檢測算法,如果φ成立,則退出算法,否則轉(zhuǎn)入步驟(4);

(4)對模型檢測返回的反例,運(yùn)行偽反例識別算法IdentAlgorithm(),如果不是偽反例,則退出算法,否則轉(zhuǎn)入步驟(5);

(5)運(yùn)行RefineAlgorithm,得到一個精化后的抽象系統(tǒng),轉(zhuǎn)入步驟(3)。

6 實(shí)驗(yàn)結(jié)果與分析

以一個銀行貸款風(fēng)險(xiǎn)評估系統(tǒng)為實(shí)驗(yàn)對象。系統(tǒng)中貸款申請客戶端是一個服務(wù)組合接口,貨款申請者通過這一接口向組合內(nèi)銀行提供的Web服務(wù)申請貸款,當(dāng)貸款額小于10 000元時,這個Web服務(wù)向風(fēng)險(xiǎn)評估Web服務(wù)請求評估風(fēng)險(xiǎn),否則向評估專家Web服務(wù)請求評估風(fēng)險(xiǎn)。當(dāng)評估結(jié)果低時銀行接受貸款請求,否則銀行拒絕貸款。設(shè)置系統(tǒng)中可以受理的貸款額范圍分別為9 000元～11 000元和5 000元～15 000元并分別進(jìn)行實(shí)驗(yàn)。實(shí)驗(yàn)平臺為:Intel Pentium 4處理器,主頻3.00 GHz;1 GB內(nèi)存;Ubuntu 12.04操作系統(tǒng);模型檢測工具M(jìn)CTK-1.0.1。實(shí)驗(yàn)結(jié)果如表1所示。

表1 MCTK模擬銀行貸款風(fēng)險(xiǎn)評估系統(tǒng)實(shí)驗(yàn)結(jié)果

從表1可以看出,不管貸款金額的范圍有多大,采用抽象技術(shù)的驗(yàn)證時間都為0.023 s,并且遠(yuǎn)小于未采用抽象技術(shù)的驗(yàn)證時間,表明本文采用抽象技術(shù)的服務(wù)組合驗(yàn)證比不采用抽象技術(shù)的服務(wù)驗(yàn)證性能更優(yōu)。

7 結(jié)束語

在研究現(xiàn)有基于多主體模型檢測驗(yàn)證Web服務(wù)組合的基礎(chǔ)上,本文提出采用抽象技術(shù)的驗(yàn)證方法,該抽象方法是一種圖狀反例向?qū)У某橄笈c精化方法,實(shí)驗(yàn)結(jié)果表明其在很大程度上緩解了基于多主體模型檢測的Web服務(wù)組合驗(yàn)證中的狀態(tài)爆炸問題,性能明顯優(yōu)于不采用優(yōu)化技術(shù)的驗(yàn)證方法。本文抽象方法與Clarke反例向?qū)У某橄螅?1］類似,不同的是本文提出時態(tài)認(rèn)知邏輯的圖狀反例以及此類反例向?qū)У某橄?并且解決了多主體系統(tǒng)的抽象,而Clarke的方法只支持傳統(tǒng)有限狀態(tài)系統(tǒng)抽象。與Lomuscio抽象方法［12］相比,本文采用的多主體系統(tǒng)的Kripke結(jié)構(gòu)較Lomuscio采用的解釋系統(tǒng)形式化程度更高,因此抽象效果更好。

由于大多數(shù)Web服務(wù)組合方案有實(shí)時性建模和驗(yàn)證需求,因此今后將在本文研究的基礎(chǔ)上進(jìn)一步研究多主體實(shí)時系統(tǒng)的模型檢測和抽象方法,并將其應(yīng)用于Web服務(wù)組合的實(shí)時性驗(yàn)證。

［1]駱翔宇,譚 征,蘇開樂,等.一種基于認(rèn)知模型檢測的Web服務(wù)組合驗(yàn)證方法［J］.計(jì)算機(jī)學(xué)報(bào),2011, 34(6):1041-1061.

［2]Clarke E M,Peled D G.Model Checking［M］.Boston, USA:MIT Press,1999.

［3]Nakajima S.Model-checking Behavioral Specification of BPEL Applications［C］//Proceedings of WCE’06.Washington D.C.,USA:IEEE Press,2006:89-105.

［4]Diaz G,Pardo J J,Cambronero M E,et al.Automatic TranslationofWs-cdlChoreographiestoTimed Automata［M］//Bravetti M,Kloul L,Zavattaro G.Formal Techniques for Computer Systems and Business Processes.Berlin,Germany:Springer,2005:230-242.［5]Fu Xiang,Bultan T,Su Jianwen.Analysis of Interacting BPEL Web Services［C］//Proceedings of the 13th InternationalConferenceonWorldWideWeb.New York,USA:ACM Press,2004:621-630.

［6]Lomuscio A,Solanki M.Towards an Agent Based Approach for Verification of OWL-S Process Models［M］// Aroyo L,Traverso P,Ciravegna F,et al.The Semantic Web:ResearchandApplications.Berlin,Germany: Springer,2009:578-592.

［7]Lomuscio A,Qu H,Solanki M.Towards Verifying Compliance in Agent-based WebServiceCompositions［C］//Proceedings of the 7th International Joint Conference onAutonomousAgentsandMultiagent Systems.Washington D.C.,USA:IEEE Press,2008: 265-272.

［8]駱翔宇,陳 艷.Web服務(wù)的形式化驗(yàn)證［J］.計(jì)算機(jī)工程,2010,36(5):257-259.

［9]駱翔宇,王 昆,王鳳釵.一種Web服務(wù)組合的認(rèn)知模型檢測方法［J］.小型微型計(jì)算機(jī)系統(tǒng),2011,32(12): 2041-2047.

［10]Clarke E M,Grumberg O,Long D E.Model Checking and Abstraction［J］.ACM Transactions on Programming Languages and Systems,1994,16(5):1512-1542.

［11]Clarke E,Grumberg O,Jha S,et al.Counterexampleguided Abstraction Refinement for Symbolic Model Checking［J］.Journal of the ACM,2003,50(5): 752-794.

［12]Cohen M,Dam M,Lomuscio A,et al.Abstraction in Model Checking Multi-agent Systems［C］//Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems.New York,USA:ACM Press,2009:945-952.

［13]Su K,Sattar A,Luo X.Model Checking Temporal Logics of Knowledge Via OBDDs［J］.The Computer Journal,2007,50(4):403-420.

編輯 陸燕菲

Verification of Web Services Based on MAS Model Checking and Abstraction

XU Xingwang1,LUO Xiangyu1,2
(1.College of Computer Science&Technology,Huaqiao University,Xiamen 361021,China;
2.Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004,China)

Web services composition is a key technology to solve cross-organizational business process integrations.However,it is hard to ensure its trusted properties(including correctness,reliability,safety),because of the loosely coupled development paradigm and open Internet running environment.To solve this problem,this paper proposes a formal verification and abstraction method for Web services composition based on model checking Multi-Agent Systems (MAS)and refinement.By applying the method of the graph-like counterexample guided abstraction and refinement on MCTK,it greatly reduces the state explosion problem of model checking.The correctness of the method is proved theoretically.Recording to the experimental results of which translates a credit risk assessment Web services to a MAS programmed by input language of MCTK then model checks both abstracted and un-abstracted MAS,the Web services verification based on proposed method works much more efficiently than the normal verification based on MAS model checking.

Web services composition;Multi-Agent System(MAS);model checking;graph-like counterexample; abstraction;refinement

許興旺,駱翔宇.基于MAS模型檢測與抽象的Web服務(wù)驗(yàn)證［J］.計(jì)算機(jī)工程,2015,41(3):26-31,36.

英文引用格式:Xu Xingwang,Luo Xiangyu.Verification of Web Services Based on MAS Model Checking and Abstraction［J］.Computer Engineering,2015,41(3):26-31,36.

1000-3428(2015)03-0026-06

:A

:TP311

10.3969/j.issn.1000-3428.2015.03.005

國家自然科學(xué)基金資助面上項(xiàng)目(61170028);華僑大學(xué)中青年教師科研提升計(jì)劃基金資助項(xiàng)目(ZQN-YX109);華僑大學(xué)高層次人才科研啟動基金資助項(xiàng)目(11BS108);廣西可信軟件重點(diǎn)實(shí)驗(yàn)室基金資助項(xiàng)目(kx201323)。

許興旺(1989-),男,碩士,主研方向:Web服務(wù)組合,模型檢測技術(shù);駱翔宇(通訊作者),副教授。

2014-02-28

:2014-04-25E-mail:decemberxf@163.com