[發(fā)明專利]一種基于約束求解器的服務(wù)組合驗證方法

在審

• 申請?zhí)枺?/td>: 201510051679.1
• 申請日: 2015-01-30
• 公開（公告）號: CN104598619A
• 公開（公告）日: 2015-05-06
• 發(fā)明（設(shè)計）人: 張迎周;馬鳳嬌;居友道;滕慶亞;徐曼青;孫韋翠
• 申請（專利權(quán)）人: 南京郵電大學(xué)
• 主分類號: G06F17/30
• 分類號: G06F17/30;H04L29/08
• 代理公司: 南京知識律師事務(wù)所 32207
• 代理人: 汪旭東

技術(shù)領(lǐng)域

本發(fā)明給出了一種基于約束求解器的Web服務(wù)組合驗證方法的設(shè)計方案，主要解決Web服務(wù)組合驗證正確性的問題，屬于Web服務(wù)組合驗證領(lǐng)域。

背景技術(shù)

隨著計算機(jī)網(wǎng)絡(luò)跨越式發(fā)展和分布式系統(tǒng)的不斷創(chuàng)新推進(jìn)，由于Web服務(wù)(Web?Services)成功結(jié)合了過去的設(shè)計要素，采用概念和技術(shù)創(chuàng)新的設(shè)計理念和設(shè)計元素，現(xiàn)在已被計算機(jī)界廣泛認(rèn)可并成為新的研究熱點?，F(xiàn)在網(wǎng)絡(luò)上的Web服務(wù)數(shù)目日益增加，但是為了能夠重用服務(wù)，單個Web服務(wù)一般都只實現(xiàn)特定的功能，難以滿足企業(yè)的復(fù)雜應(yīng)用需求。如果能將已經(jīng)存在的Web服務(wù)按照一定的業(yè)務(wù)流程合理組合起來，形成一個復(fù)合Web服務(wù)，就能夠提供更加強大的功能，滿足用戶實際的需要。

Web服務(wù)組合技術(shù)可提供功能豐富的業(yè)務(wù)流程，但是如何判斷組合的Web服務(wù)是否滿足用戶的業(yè)務(wù)需求，如何判斷組合的Web服務(wù)在運行中有沒有出現(xiàn)問題，企業(yè)在真正應(yīng)用Web服務(wù)組合解決實際問題前必須認(rèn)真考慮這些問題。Web服務(wù)組合技術(shù)由于推出時間比較短，體系結(jié)構(gòu)、技術(shù)實現(xiàn)等方面還不是很完善，因而在實際應(yīng)用中會面臨著各種挑戰(zhàn)。由于網(wǎng)絡(luò)上的Web服務(wù)是由不同的組織機(jī)構(gòu)基于不同的平臺使用不同的語言開發(fā)的，這使得Web服務(wù)具有異構(gòu)性和多變性的特點，組合服務(wù)可能會因為其中的某個Web服務(wù)出現(xiàn)異常變化而無法正常運行。事實上，不管是人工設(shè)計的還是自動創(chuàng)建完成的服務(wù)組合都可能存在多種問題，比如可能發(fā)生死鎖、活鎖和狀態(tài)不可達(dá)等問題。因此Web服務(wù)組合在投入實際應(yīng)用前必須先進(jìn)行驗證，以保證組合服務(wù)的正確性。

當(dāng)前用來描述Web服務(wù)和Web服務(wù)組合的語言都是半形式化的，難以保證正確性，當(dāng)服務(wù)組合出現(xiàn)錯誤時，很難檢測出錯誤原因，因此需要有形式化的方法來驗證Web服務(wù)組合是否正確。Web服務(wù)組合可以使用不同的形式化方法描述和驗證，當(dāng)前研究多集中于使用Petri網(wǎng)、自動機(jī)理論和進(jìn)程代數(shù)這三種方法。

Petri網(wǎng)是一種特別適合分析和驗證分布式系統(tǒng)的形式化建模方法，它的優(yōu)點是形象直觀、語義嚴(yán)格并且有數(shù)學(xué)理論作為基礎(chǔ)，可以用來對控制流和數(shù)據(jù)流進(jìn)行形式化建模。Petri網(wǎng)也可以用來描述分布、并發(fā)、非確定性的信息系統(tǒng)，提供了一種定性和定量分析方法以及可操作語義。

自動機(jī)理論就是利用有限自動機(jī)對BPEL描述的服務(wù)組合流程進(jìn)行建模，然后檢驗該流程的安全性和活性等屬性，再根據(jù)檢驗結(jié)果判斷該服務(wù)組合流程是否正確。

進(jìn)程代數(shù)是一種使用代數(shù)方法研究通信并發(fā)系統(tǒng)的理論，包括通信順序進(jìn)程、通信系統(tǒng)演算和π演算等，非常適合用來描述和驗證并發(fā)系統(tǒng)。尤其是π演算可以傳遞變量、值和通道名，具有建立新通道的能力，特別適合用來描述分布式松禍合的并發(fā)系統(tǒng)。

采用Petri網(wǎng)或者自動機(jī)對服務(wù)組合進(jìn)行描述時盡管較為直觀，但在服務(wù)流程規(guī)模變大、服務(wù)數(shù)量變多、服務(wù)間交互變復(fù)雜的情況下，這兩類方法的復(fù)雜度隨著服務(wù)組合規(guī)模的增大而急劇增大。與此相比，基于進(jìn)程代數(shù)的方法因為采用了表達(dá)式的描述方法，所以表達(dá)能力強且形式簡潔，另外進(jìn)程代數(shù)特別是π演算中的行為理論為服務(wù)驗證提供了很好的理論基礎(chǔ)，但π演算比較缺乏直觀的圖形表示，工具支持也不是很多。通過對以往研究進(jìn)展的研究，本發(fā)明提出通過解析WSDL，BPEL文檔得到約束條件，在通過約束求解器Z3求解從而實現(xiàn)驗證。

參考文獻(xiàn)：

[1]Wonhong?Nam,Hyunyoung?Kil,Dongwon?Lee.Type-Aware?Web?Service?Composition?Using?Boolean?Satisfiability?Solver.[C]//proceedings?of?IEEE?Conference?on?E-Commerce?Technology.Washington,D.C.,USA?IEEE,2008:331-334

[2]John?Kodumal,Alexander?Aiken.The?set?constraint/CFL?reachability?connection?in?practice[J].Sigplan?Notices-SIGPLAN,2004,39(6):207-218

發(fā)明內(nèi)容

技術(shù)問題：本發(fā)明的目的是提出一種基于約束求解器的服務(wù)組合驗證方法。該方法從利用BPEL組合Web服務(wù)出發(fā)，對BPEL文檔進(jìn)行分析，構(gòu)建一個能表示服務(wù)之間的執(zhí)行關(guān)系和約束關(guān)系的控制流程圖。然后利用約束求解器驗證用戶提供的初始條件和目標(biāo)輸出及服務(wù)之間的約束關(guān)系，以此判斷這個Web服務(wù)組合的正確性，從而達(dá)到最終驗證服務(wù)組合的目的。