基于分層著色Petri網(wǎng)的Web服務動態(tài)組合建模與驗證.pdf

1、隨著Web服務技術的發(fā)展,網(wǎng)上發(fā)布的Web服務的數(shù)量將越來越多,當單個服務無法滿足用戶的需求時,需要將多個功能有限的服務進行服務組合,產(chǎn)生增值服務。手工地去組合這些Web服務,不便于對服務組合依據(jù)用戶需求變化,進行動態(tài)調(diào)整,所以迫切需要對這些服務進行動態(tài)組合。Web服務本體描述語言OWL-S所描述的Web服務流程,使得Web服務包含機器可讀的語義信息,可以實現(xiàn)Web服務的自動發(fā)現(xiàn)、組合、執(zhí)行和監(jiān)控。但動態(tài)服務組合卻是一個復雜而易錯的過程

2、,現(xiàn)有的組合規(guī)范缺乏有效的驗證機制,因此需要建立Web服務組合的形式化描述模型,利用對形式化模型的分析,驗證方法來檢驗Web服務動態(tài)組合的正確性和有效性。
　　 目前已有一些形式化驗證方法,主要有基于進程代數(shù)、自動機和Petri網(wǎng)。但是進程代數(shù)和自動機方法只是停留在語法層面,對語義信息描述不夠,且建模過程復雜,模型抽象,缺乏直觀的圖形表示。由于基本Petri網(wǎng)沒有顏色和分層的概念,不能精確表達Web服務不同類型的數(shù)據(jù),而且對于大

3、規(guī)模復雜系統(tǒng),容易出現(xiàn)狀態(tài)空間爆炸問題。
　　 本文提出一種利用分層著色Petri網(wǎng)(HCPN)對以OWL-S描述的Web服務組合流程建模和驗證的方法。首先研究基于OWL-S的語義Web服務動態(tài)組合流程,得到Web服務組合過程模型;然后提出OWL-S描述的Web服務組合流程中的原子過程,復合過程以及各控制結(jié)構(gòu)向Petri網(wǎng)轉(zhuǎn)化的規(guī)則,得到Web服務動態(tài)組合過程模型對應的分層著色Petri網(wǎng)模型;最后利用CPN Tools工具對建

4、立的CPN模型進行動態(tài)模擬仿真,并通過狀態(tài)空間機制驗證模型的有界性、可達性、活性(探測有無死鎖)等各項性能。從而達到驗證Web服務組合正確性和有效性的目的。
　　 分層著色Petri網(wǎng)(HCPN)建模,彌補了一般Petri網(wǎng)的不足,引入不同顏色的token以及token數(shù)的變化來表示OWL-S模型中的IOPE,可以更好的刻畫Web服務的控制流和數(shù)據(jù)流,引入分層概念,可以簡化模型,對于大型復雜系統(tǒng)可以分成一些子網(wǎng),每個階段獨立驗證