許興旺,駱翔宇,2

(1.華僑大學計算機科學與技術學院,福建廈門361021;2.桂林電子科技大學廣西可信軟件重點實驗室,廣西桂林541004)

基于MAS模型檢測與抽象的Web服務驗證

許興旺1,駱翔宇1,2

(1.華僑大學計算機科學與技術學院,福建廈門361021;2.桂林電子科技大學廣西可信軟件重點實驗室,廣西桂林541004)

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

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

1 概述

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

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

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

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

2 基本概念

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

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

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

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

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

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

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

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

圖1 Kiφ的圖狀反例

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

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

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

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

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

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

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

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

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

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

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

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

轉(zhuǎn)換函數(shù)A將V上的任意n元謂詞P轉(zhuǎn)換成上的n元謂詞函數(shù)。其中,是近似抽象系統(tǒng)的系統(tǒng)變量集合,只不過其定義域為。轉(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′)。

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

根據(jù)文獻［11］對這種初始抽象系統(tǒng)生成方法做了一些改進,具體如下:因為輸入語言的程序中包含對系統(tǒng)遷移條件的描述,以及待驗證性質(zhì)的描述,并且遷移條件由原子命題的布爾運算構成,驗證的性質(zhì)在布爾運算基礎上又加了時態(tài)算子和認知算子,所以,從輸入語言程序中可以抽取出一個原子命題集合。令A表示這個集合。將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)邏輯公式,其原因及消除偽反例的方法在文獻［11］中已經(jīng)敘述。

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

圖2 初始抽象實例

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

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

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

算法1splitCounterexample Algorithm

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

算法2splitEP Algorithm

算法3PolyRefineEpistemic Algorithm

5 Web服務組合的驗證

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

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

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

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

算法4Verification Algorithm

Verification(Composition)//Composition是待驗證Web服務組合

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

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

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

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

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

6 實驗結(jié)果與分析

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

表1 MCTK模擬銀行貸款風險評估系統(tǒng)實驗結(jié)果

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

7 結(jié)束語

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

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

［1]駱翔宇,譚 征,蘇開樂,等.一種基于認知模型檢測的Web服務組合驗證方法［J］.計算機學報,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服務的形式化驗證［J］.計算機工程,2010,36(5):257-259.

［9]駱翔宇,王 昆,王鳳釵.一種Web服務組合的認知模型檢測方法［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服務驗證［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

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

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

2014-02-28

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