李靖 崔仲遠(yuǎn)

摘 要： 針對Web服務(wù)組合的有效性驗證問題，提出了一種基于服務(wù)分組和調(diào)用軌跡的Web服務(wù)組合形式化驗證方案。首先，基于服務(wù)調(diào)用順序，利用提出的Web服務(wù)集分組（WSSG）算法將候選Web服務(wù)劃分為幾個子集，并結(jié)合調(diào)用軌跡編排這些子集組成WSSG圖，作為系統(tǒng)的抽象模型；然后，推理出系統(tǒng)所需的預(yù)期交互規(guī)范，并利用線性時序邏輯（LTL）來描述交互規(guī)范；最后，通過檢測模型是否符合交互規(guī)范來驗證組合模型的可行性。實驗結(jié)果表明，該方案能夠有效驗證Web服務(wù)組合的正確性，且避免了死鎖現(xiàn)象。

關(guān)鍵詞： Web服務(wù)組合驗證； 建模； 調(diào)用軌跡； 線性時序邏輯

中圖分類號： TN911?34； TP311 文獻(xiàn)標(biāo)識碼： A 文章編號： 1004?373X（2016）05?0126?05

0 引 言

Web服務(wù)是一種基于網(wǎng)絡(luò)的、分布式的模塊化組件。由于單一Web服務(wù)功能有限，所以需要將不同的Web服務(wù)進(jìn)行組合，提供更為強(qiáng)大的功能，滿足不同用戶的需求[1]。由于Web服務(wù)組合常用于跨平臺、跨組織的分布式環(huán)境，服務(wù)組合在執(zhí)行過程中可能會受到通信模式的變化、服務(wù)基礎(chǔ)設(shè)施失效等問題的影響，所以有必要對Web服務(wù)組合的有效性和可靠性進(jìn)行驗證[2]。

目前，Web服務(wù)組合的驗證方法主要包括模型檢查、Petri網(wǎng)、Pi?演算、遺傳算法、行為時序邏輯（TLA）和基于推理的交互時序邏輯等[3]。文獻(xiàn)[4]提出一種Web服務(wù)組合的正確性驗證方法，即采用軟件體系結(jié)構(gòu)描述語言XYZ/ADI，描述Web服務(wù)組合，其性質(zhì)（規(guī)范）用CTL公式表示，最后用模型檢測工具UPPAAL驗證Web服務(wù)組合的正確性。文獻(xiàn)[5]提出一種基于Petri網(wǎng)理論的Web服務(wù)組合建模方法，即對服務(wù)組合進(jìn)行形式化建模，通過分析Web服務(wù)網(wǎng)的可達(dá)性和活性驗證Web服務(wù)組合。文獻(xiàn)[6]利用Pi?演算對Web服務(wù)組合建立形式化模型，定義了Pi?演算到BPEL4WS的概念映射，給出了基于Pi?演算的形式化描述。然而，這些方法都有自身的缺陷，例如：中間語言的參與、無法捕獲遞歸組合、更多的時間和空間復(fù)雜性等。

模型檢測（Model Checking，MC）是一種形式化驗證方法，用狀態(tài)遷移系統(tǒng)表示系統(tǒng)的行為，用時序邏輯公式描述系統(tǒng)的屬性[7]。這樣“系統(tǒng)是否具有所期望的屬性”就轉(zhuǎn)化為數(shù)學(xué)問題“狀態(tài)遷移系統(tǒng)是否是公式的一個模型”。模型檢測方法具有自動化程度高、能夠提供反例路徑等優(yōu)勢，被廣泛應(yīng)用于Web服務(wù)組合相關(guān)屬性的驗證[8]。然而隨著系統(tǒng)規(guī)模的不斷擴(kuò)大，這種以窮盡搜索為基礎(chǔ)的方法將會產(chǎn)生狀態(tài)空間“爆炸”問題，成為驗證大規(guī)模系統(tǒng)的瓶頸[9]。

本文采用模型檢測方法，并對其存在的缺陷，提出一種新的形式化模型來推理和動態(tài)驗證Web服務(wù)組合。利用提出的Web服務(wù)集分組（Web Service Set Grouping，WSSG）算法將候選Web服務(wù)劃分為幾個子集，并將這些子集組成Web服務(wù)集分組圖（WSSG圖），作為系統(tǒng)的抽象模型；然后，將該模型轉(zhuǎn)換為交互軌跡的集合，來推理系統(tǒng)需要的預(yù)期交互規(guī)范，并利用線性時序邏輯（Linear Temporal Logic，LTL）[10]來描述交互規(guī)范；最后，通過檢測系統(tǒng)模型是否符合交互規(guī)范來驗證組合模型的可行性。 本文服務(wù)交互驗證方案主要包括兩個部分：Web服務(wù)組合系統(tǒng)建模和Web服務(wù)組合驗證。

4 結(jié) 語

本文提出了一種Web服務(wù)組合形式化驗證方法。首先，對服務(wù)組合進(jìn)行建模，利用提出的Web服務(wù)集分組（WSSG）算法將候選Web服務(wù)劃分為幾個子集，并結(jié)合調(diào)用軌跡編排這些子集組成WSSG圖，作為系統(tǒng)的抽象模型；然后，推理系統(tǒng)所需的預(yù)期交互規(guī)范，利用線性時序邏輯（LTL）來描述交互規(guī)范；最后，通過檢測模型是否符合交互規(guī)范來驗證組合模型的可行性。通過旅行社場景實驗表明，本文方案能夠有效驗證Web服務(wù)組合的正確性。

在今后的工作中，將考慮失敗任務(wù)的替代驗證和冗余校驗，來擴(kuò)展本文驗證方法。

參考文獻(xiàn)

[1] 溫濤，盛國軍，郭權(quán)，等.基于改進(jìn)粒子群算法的Web服務(wù)組合[J].計算機(jī)學(xué)報，2013，36（5）：1031?1046.

[2] 張廣泉，狄浩軍，石慧娟，等.基于擴(kuò)展自動機(jī)的服務(wù)組合靜態(tài)與動態(tài)驗證方法[J].通信學(xué)報，2012，33（z1）：1?8.

[3] KLAI K， TATA S， OCHI H. Generic and specific compatibility criteria for Web service composition： formal abstraction and modular verification approach [J]. International journal of Web services research， 2012， 9（9）： 45?68.

[4] 張廣泉，戎玫，朱雪陽，等.基于XYZ/ADL的Web服務(wù)組合描述與驗證[J].電子學(xué)報，2011，39（3）：86?93.

[5] WANG Y Y， CHEN P. Web service composition verification of safety properties： an approach based on predicate abstraction [J]. Advanced materials research， 2013， 55（4）： 2892?2899.

[6] 胡靜，饒國政，馮志勇.基于多元Pi?演算的Web服務(wù)組合描述與驗證[J].天津大學(xué)學(xué)報（自然科學(xué)與工程技術(shù)版），2013，46（6）：520?525.

[7] 駱翔宇，譚征，蘇開樂，等.一種基于認(rèn)知模型檢測的Web服務(wù)組合驗證方法[J].計算機(jī)學(xué)報，2011，34（6）：1041?1061.

[8] ZAHOOR E， MUNIR K， PERRIN O， et al. A bounded model checking approach for the verification of Web services composition [J]. International journal of Web services research， 2013， 10（4）： 62?81.

[9] CHEN T W， GENG S Y. Verification of time constraints consistency on Web service composition based on ETPN [J]. Applied mechanics and materials， 2011， 60： 1094?1099.

[10] 周寧，劉慧，王紅兵，等.采用動作時序邏輯的Web服務(wù)組合方法[J].計算機(jī)科學(xué)與探索，2011，5（3）：208?220.

[11] SUMATHI S， CHIPLUNKAR N N， ASHOK K A. Dynamic discovery of Web services using WSDL [J]. International journal of information technology and computer science， 2014， 6（10）： 56?62.

[12] DUMEZ C， BAKHOUYA M， GABER J， et al. Model?driven approach supporting formal verification for Web service composition protocols [J]. Journal of network and computer applications， 2013， 36（4）： 1102?1115.

[13] RAI G N， GANGADHARAN G R， PADMANABHAN V. Algebraic modeling and verification of Web service composition [J]. Procedia computer science， 2015， 52（1）： 675?679.

[14] KIL H， NAM W. Semantic Web service composition using formal verification techniques [C]// Proceedings of EL， DTA and UNESST 2012 Generation Information Technology Confe?rence. Gangneug： EL， DTA and UNESST， 2012： 72?79.

[15] BARYANNIS G， PLEXOUSAKIS D. Fluent calculus?based semantic Web service composition and verification using WSSL [J]. Lecture notes in computer science， 2013： 256?270.