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

許興旺,駱翔宇,2

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

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

許興旺1,駱翔宇1,2

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

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

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

1 概述

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

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

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

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

2 基本概念

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

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

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

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

3 時態認知邏輯的圖狀反例

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

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

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

圖1 Kiφ的圖狀反例

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

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

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

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

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

4 圖狀反例向導的抽象與精化

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

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

4.1 初始抽象系統的生成

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

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

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

轉換函數A將V上的任意n元謂詞P轉換成上的n元謂詞函數。其中,是近似抽象系統的系統變量集合,只不過其定義域為。轉換函數定義如下:

(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′)。

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

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

4.2 圖狀反例向導的精化

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

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

圖2 初始抽象實例

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

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

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

算法1splitCounterexample Algorithm

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

算法2splitEP Algorithm

算法3PolyRefineEpistemic Algorithm

5 Web服務組合的驗證

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

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

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

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

算法4Verification Algorithm

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

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

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

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

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

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

6 實驗結果與分析

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

表1 MCTK模擬銀行貸款風險評估系統實驗結果

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

7 結束語

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

由于大多數Web服務組合方案有實時性建模和驗證需求,因此今后將在本文研究的基礎上進一步研究多主體實時系統的模型檢測和抽象方法,并將其應用于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］.小型微型計算機系統,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