基于有色賦時(shí)Petri網(wǎng)的Web服務(wù)組合建模驗(yàn)證與測試技術(shù)研究.pdf

1、Web服務(wù)(Web Service)是一種自包含、自描述、模塊化的應(yīng)用程序，它吸收了分布式計(jì)算、網(wǎng)格計(jì)算和XML等各種技術(shù)的優(yōu)點(diǎn)，解決了異構(gòu)分布式計(jì)算以及代碼與數(shù)據(jù)重用等問題，具有高度的互操作性、跨平臺性和松耦合性，已經(jīng)在電子商務(wù)、企業(yè)應(yīng)用集成等領(lǐng)域發(fā)揮著重要作用，特別是Web服務(wù)組合技術(shù)，因其能實(shí)現(xiàn)服務(wù)的重用和增值而引起了世界范圍內(nèi)學(xué)術(shù)界和工業(yè)界的關(guān)注。
　　 Web服務(wù)組合本身是一項(xiàng)易于產(chǎn)生錯誤的任務(wù)，因?yàn)樵诮M合中候選的服務(wù)

2、之間進(jìn)行復(fù)雜的交互。Web服務(wù)業(yè)務(wù)流程執(zhí)行語言(Web Service Business Process Execution Language，WS-BPEL，簡稱BPEL)用于實(shí)現(xiàn)Web服務(wù)的組合和合并，它建立在IBM的Web服務(wù)流語言(Web Services Flow Language，WSFL)和Microsoft的XML業(yè)務(wù)流程語言(XML Business Process Language，XLANG)之上，結(jié)合了這兩種語言

3、的特性，這樣就引起了某些方面的不一致和語義的模糊；BPEL的語義是用英語定義的，這樣無法避免其二義性、模糊性和不完全性。WS-BPEL技術(shù)委員會公認(rèn)為需要對BPEL語義給出形式化定義。
　　 由于要處理并發(fā)，具有復(fù)雜特性，如補(bǔ)償處理、相關(guān)性、死路徑刪除(Dead-Path-Elimination，DPE)等，BPEL過程是容易出錯的。
　　 本文主要研究由BPEL生成的Web服務(wù)組合流程的建模、驗(yàn)證、測試問題。
　

4、　 針對BPEL流程建模，目前采用的方法有Petri網(wǎng)、SPIN工具、進(jìn)程代數(shù)、抽象狀態(tài)機(jī)和自動機(jī)等方法。本文采用賦時(shí)有色Petri網(wǎng)對BPEL流程建模。首先對BPEL的各種活動建模，將BPEL流程看作是活動的嵌套，將嵌套關(guān)系對應(yīng)于層次化有色Petri網(wǎng)的層次關(guān)系緩解了有色Petri網(wǎng)模型過于龐大以及狀態(tài)爆炸問題。本文提出的層次化有色Petri網(wǎng)的展開算法，使層次化Petri網(wǎng)可以展開成等價(jià)的非層次化Petri網(wǎng)，能夠呈現(xiàn)出模型的細(xì)節(jié)

5、。本文還完善了層次化有色Petri網(wǎng)的定義。
　　 Web服務(wù)的形式化驗(yàn)證是近年來才開始進(jìn)入研究領(lǐng)域的，但是已經(jīng)獲得了很多研究人員的關(guān)注。針對BPEL模型驗(yàn)證，本文給出了利用有色Petri網(wǎng)的屬性對BPEL流程的基本屬性進(jìn)行驗(yàn)證，使用擴(kuò)展時(shí)態(tài)邏輯ASK-CTL來描述要驗(yàn)證的屬性，對模型的動態(tài)屬性進(jìn)行驗(yàn)證的一種方法。為了處理程序驗(yàn)證過程中出現(xiàn)的狀態(tài)爆炸問題，本文還對謂詞抽象技術(shù)和惰性抽象技術(shù)進(jìn)行了研究，將CP-nets的狀態(tài)圖生成

6、過程，以及狀態(tài)圖的謂詞抽象過程合為一體，在狀態(tài)生成過程中形成抽象狀態(tài)圖，從而避免了狀態(tài)爆炸問題。本文將惰性抽象用于BPEL流程的安全性驗(yàn)證方法CEGAR中，優(yōu)化了“抽象-驗(yàn)證-反例”中的前兩個步驟，使得這個方法可以用于規(guī)模較大的程序上。
　　 Web服務(wù)為分布式計(jì)算提供了靈活的、可重用的、松散耦合的模型，BPEL是半形式化的、具有復(fù)雜特性的、易含有錯誤行為的語言。在Web服務(wù)發(fā)布之前對服務(wù)進(jìn)行驗(yàn)證、測試，確認(rèn)服務(wù)符合設(shè)計(jì)模型是必