李靖 崔仲遠(yuǎn)

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

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

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

0 引 言

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

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

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

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

4 結(jié) 語(yǔ)

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

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

參考文獻(xiàn)

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

[2] 張廣泉，狄浩軍，石慧娟，等.基于擴(kuò)展自動(dòng)機(jī)的服務(wù)組合靜態(tài)與動(dòng)態(tài)驗(yàn)證方法[J].通信學(xué)報(bào)，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] 張廣泉，戎玫，朱雪陽(yáng)，等.基于XYZ/ADL的Web服務(wù)組合描述與驗(yàn)證[J].電子學(xué)報(bào)，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] 胡靜，饒國(guó)政，馮志勇.基于多元Pi?演算的Web服務(wù)組合描述與驗(yàn)證[J].天津大學(xué)學(xué)報(bào)（自然科學(xué)與工程技術(shù)版），2013，46（6）：520?525.

[7] 駱翔宇，譚征，蘇開(kāi)樂(lè)，等.一種基于認(rèn)知模型檢測(cè)的Web服務(wù)組合驗(yàn)證方法[J].計(jì)算機(jī)學(xué)報(bào)，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] 周寧，劉慧，王紅兵，等.采用動(dòng)作時(shí)序邏輯的Web服務(wù)組合方法[J].計(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.