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

在審

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

1.一種基于約束求解器的服務(wù)組合驗(yàn)證方法，其特征在于該方法包括Web服務(wù)文檔解析、Web服務(wù)約束條件提取和Web服務(wù)驗(yàn)證三部分，該方法包含的步驟如下：

1)對(duì)WSDL文檔進(jìn)行解析

WSDL是一種web?services的描述語(yǔ)言，使用開(kāi)源工具WSDL4J將WSDL解析為DOM樹(shù)，然后分別提取types,message,portType,binding,service的tag信息，為了提取WSDL中的變量約束信息，需要提取message標(biāo)簽信息以獲取message中包含的part信息，用于在BPEL中查找對(duì)應(yīng)變量約束；在獲取types標(biāo)簽信息時(shí)，需要區(qū)分簡(jiǎn)單元素類(lèi)型和復(fù)雜元素類(lèi)型，對(duì)于簡(jiǎn)單元素類(lèi)型，直接獲取元素的name,type屬性值；對(duì)于復(fù)雜元素類(lèi)型，需要對(duì)其進(jìn)行特殊處理：由于WSDL4J中沒(méi)有對(duì)復(fù)雜類(lèi)型進(jìn)行處理的函數(shù)，需要自行解析，而根據(jù)復(fù)雜類(lèi)型的XML?schema定義，只需迭代獲取子標(biāo)簽的內(nèi)容即可得到復(fù)雜類(lèi)型標(biāo)簽中包含元素的詳細(xì)定義；

2)對(duì)BPEL文檔進(jìn)行解析

BPEL是一種用XML編寫(xiě)的編程語(yǔ)言，

在BPEL的解析階段，先將BPEL解析為DOM樹(shù)，由BPEL?Version?2.0的定義可知，BPEL的根節(jié)點(diǎn)為<process>，<process>的子節(jié)點(diǎn)包括<extensions>,<import>,<partnerLinks>,<messageExchanges>,<variables>,<correlationSets>,<faultHandlers>,<eventHandlers>以及業(yè)務(wù)執(zhí)行活動(dòng)等標(biāo)簽；另外，在BPEL的解析階段，還需要提取業(yè)務(wù)執(zhí)行流程，具體的過(guò)程為：找到根節(jié)點(diǎn)<process>的所有子節(jié)點(diǎn)，然后根據(jù)<process>的所有子節(jié)點(diǎn)名，即可查找到該BPEL中定義的業(yè)務(wù)執(zhí)行流程子節(jié)點(diǎn)，最后提取出業(yè)務(wù)執(zhí)行流程中服務(wù)調(diào)用、變量賦值等關(guān)系得到一個(gè)執(zhí)行流程中間文件；

3)將提取的中間文件，利用在cygwin中安裝tools4bpel工具將bpel文件轉(zhuǎn)化成控制流圖即CFG圖；

4)建立一個(gè)一階公式描述CFG圖

由BPEL?Version?2.0的定義可知活動(dòng)類(lèi)型包括<receive>,<reply>,<invoke>,<assign>,<sequence>,<if>,<while>,<repeatUntil>,<forEach>,<pick>,<flow>,<scope>,<throw>,<exit>,<wait>,<empty>,<compensate>,<compensateScope>,<rethrow>,<validate>,<extensionActivity>，其中<throw>,<exit>,<wait>,<empty>,<compensate>,<compensateScope>,<rethrow>,<validate>,<extensionActivity>的活動(dòng)主要用于拋出異常、結(jié)束業(yè)務(wù)執(zhí)行流程、等待、數(shù)據(jù)驗(yàn)證等特殊情況，未加考慮；

CFG圖描述的是業(yè)務(wù)執(zhí)行流程，在對(duì)其進(jìn)行處理時(shí)，主要目標(biāo)是提取業(yè)務(wù)執(zhí)行流程以及活動(dòng)中變量的賦值關(guān)系，所以在解析BPEL時(shí)，根據(jù)業(yè)務(wù)執(zhí)行流程、活動(dòng)類(lèi)型、變量的賦值關(guān)系以及從WSDL中提取的變量約束條件，自動(dòng)化生成XML文檔用以保存簡(jiǎn)化的BPEL；

然后利用模型檢查中的方法，根據(jù)不同的活動(dòng)類(lèi)型對(duì)業(yè)務(wù)執(zhí)行流程進(jìn)行改寫(xiě)，使得業(yè)務(wù)執(zhí)行流程可以使用if,assignment,assertions語(yǔ)句以及邏輯運(yùn)算符表示，根據(jù)業(yè)務(wù)執(zhí)行流程中的活動(dòng)分類(lèi)情況，改寫(xiě)規(guī)則如下：

·<receive>用于接收匹配的message信息，從而獲取輸入?yún)?shù)，該活動(dòng)為基本活動(dòng)，可直接使用賦值表達(dá)式將輸入?yún)?shù)賦值給相應(yīng)的變量；

·<reply>用于發(fā)送message信息，從而輸出活動(dòng)參數(shù)，該活動(dòng)為基本活動(dòng)，可直接使用賦值表達(dá)式將輸出變量的值賦值給輸出參數(shù)；

·<invoke>用于調(diào)用PartnerLink中定義的其它Web服務(wù)，由于測(cè)試人員只能根據(jù)portType獲取對(duì)應(yīng)的接口說(shuō)明，無(wú)法獲取將要調(diào)用的Web服務(wù)的源代碼，因此無(wú)法獲取被調(diào)用的Web服務(wù)中的約束條件，只能使用BPEL內(nèi)置函數(shù)getVariableData()來(lái)獲取調(diào)用Web服務(wù)后的參數(shù)值，并將得到的值賦值給相應(yīng)的參數(shù)；

·<assign>活動(dòng)用于對(duì)BPEL活動(dòng)調(diào)用的變量賦值，該活動(dòng)通常包括多于1個(gè)的<copy>子標(biāo)簽，用于指明賦值操作的對(duì)象，在獲取賦值對(duì)象后，即可得到<assign>活動(dòng)的賦值表達(dá)式；

·<sequence>活動(dòng)定義了BPEL中一個(gè)順序執(zhí)行的活動(dòng)集合，對(duì)于一個(gè)<sequence><A1/><A2/><A3/></sequence>活動(dòng)，各個(gè)子活動(dòng)之間是順序執(zhí)行的關(guān)系，因此其條件范式為：A1；A2；A3；

·<if>活動(dòng)定義了BPEL中一個(gè)選擇執(zhí)行的活動(dòng)類(lèi)型，

·<while>活動(dòng)定義了BPEL中一個(gè)循環(huán)操作，對(duì)于一個(gè)<while><condition/><activity/></while>活動(dòng)，由于while(e){I}→if(e){I?while(e){I}}成立，因此將<while>活動(dòng)轉(zhuǎn)變?yōu)椋?/p>

·<pick>活動(dòng)用于定義BPEL中一個(gè)選擇操作，對(duì)于活動(dòng)<pick><A1/><A2/><A3/></pick>，執(zhí)行時(shí)只能選取其中一個(gè)活動(dòng)，因此其對(duì)應(yīng)的邏輯表達(dá)式為：

·<flow>活動(dòng)用于定義BPEL中一個(gè)并發(fā)操作，對(duì)于活動(dòng)<flow><A1/><A2/></flow>,可能的活動(dòng)執(zhí)行次序有：{A1；A2}，{A2；A1}，在程序執(zhí)行時(shí)，每次只能有一種活動(dòng)執(zhí)行次序?yàn)檎妫虼饲笆?lt;flow>活動(dòng)對(duì)應(yīng)的邏輯表達(dá)式為：

通過(guò)上面改寫(xiě)之后再通過(guò)規(guī)范化算法，得到只包含邏輯運(yùn)算符及if,assignment,assertions語(yǔ)句；

5)結(jié)合約束求解器對(duì)輸入的語(yǔ)法要求，生成符合求解器輸入格式的約束條件；

6)將上幾步中生成的約束條件及邏輯公式代入約束求解器，進(jìn)行驗(yàn)證。