基于擴展顏色Petri網(wǎng)的服務組合邏輯模型的構建與驗證.pdf

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

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

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