基于擴(kuò)展顏色Petri網(wǎng)的服務(wù)組合邏輯模型的構(gòu)建與驗(yàn)證.pdf

1、隨著Internet在全球的發(fā)展，基于網(wǎng)絡(luò)的分布式應(yīng)用越來越呈現(xiàn)出多樣性和復(fù)雜性。其中，統(tǒng)一的服務(wù)注冊、發(fā)現(xiàn)、綁定和集成機(jī)制，成為廣域環(huán)境中實(shí)現(xiàn)互操作的一種有效方式，并得到學(xué)術(shù)界和產(chǎn)業(yè)界的廣泛認(rèn)可。單個的Web服務(wù)能夠提供的功能的有限性使得將共享的Web服務(wù)組合起來，以提供功能更為強(qiáng)大的服務(wù)成為必要，這促使Web服務(wù)組合研究的興起。服務(wù)組合的結(jié)果表現(xiàn)為一個自動執(zhí)行的處理流程。協(xié)調(diào)一個流程中服務(wù)調(diào)用的順序、對服務(wù)之間的數(shù)據(jù)流進(jìn)行管理，都需

2、要提供有效性、可靠性和可度量性的支持。如何利用工具對Web服務(wù)組合進(jìn)行建模，進(jìn)而進(jìn)行分析、驗(yàn)證和仿真成為當(dāng)前急待解決的問題。 針對上述問題本文選用Petri 網(wǎng)作為服務(wù)組合的建模和驗(yàn)證工具。Petri網(wǎng)是一個圖形化的數(shù)學(xué)建模工具。一方面利用圖形化方式來描述流程，另一方面利用其形式化分析技術(shù)對所建立模型的正確性進(jìn)行分析驗(yàn)證。本文以顏色Petri網(wǎng)為基礎(chǔ)進(jìn)行擴(kuò)展，提出了一種基于擴(kuò)展顏色Petri網(wǎng)的服務(wù)組合邏輯模型的構(gòu)建方法。在這個

3、方法中，設(shè)計了一個包括靜態(tài)和動態(tài)兩個方面的元模型，利用元模型的這兩個方面的一致性，解決了服務(wù)組合過程中控制流、數(shù)據(jù)流、以及特殊的I/O流無法在同一個圖中表示的問題。在驗(yàn)證方面，本文在Petri網(wǎng)已有性質(zhì)和驗(yàn)證方法的基礎(chǔ)上，采用圖形和線性代數(shù)技術(shù)分析和驗(yàn)證了基于Petri網(wǎng)的服務(wù)組合邏輯應(yīng)包含的性質(zhì)：可達(dá)性、有界性、活性和互斥性。最后給出了全部性質(zhì)驗(yàn)證過程及其重要步驟地實(shí)現(xiàn)的算法，以及對實(shí)驗(yàn)數(shù)據(jù)、平臺和結(jié)果的分析。對這些理論和實(shí)驗(yàn)的總結(jié)為