《Petri網(wǎng)原理與應(yīng)用》讀書筆記

1、Petri網(wǎng)原理與應(yīng)用讀書筆記1 傳統(tǒng) Petri 網(wǎng)介紹Carl Adam Petri 教授于 1962 年在博士論文用自動機理論通信中首次提出的一種自動機網(wǎng)狀結(jié)構(gòu)模型，擁有能恰當處理因果上的不存在依賴性的并行現(xiàn)象和表示不確定性的選擇的能力，以及以系統(tǒng)模型用網(wǎng)狀圖形表示的方法。傳統(tǒng)的 Petri 網(wǎng)是簡單的過程模型，由兩種節(jié)點：庫所和變遷，有向弧，以及令牌等元素組成的。相關(guān)概念：（1）transition enabled（變遷的就緒）：當且僅當 transition 的每一個輸入 place 都至少有一個 token 的時候，變遷就緒，可以實施。（2）transition firing（變遷

2、的實施）：變遷實施的時候它的每一個輸入庫所托肯減少一個，并使它的每一個輸出庫所的托肯增加一個。圖1.1 顯示了 Petri 網(wǎng)的基本建模，其中圓圈表示 place；矩形表示 transition；存在于 place 中用的 token 用黑點表示。用簡單圖形較好的表示并發(fā)、同步、因果等關(guān)系。以網(wǎng)圖的方式簡潔、直觀的模擬離散事件系統(tǒng)。目前已得到廣泛應(yīng)用,有限狀態(tài)機、通信協(xié)議、同步控制、生產(chǎn)系統(tǒng)、形式語言、多處理器系統(tǒng)等建模中。通訊協(xié)議的驗證是Petri網(wǎng)應(yīng)用最為成功的領(lǐng)域之一最初應(yīng)用在70年代初期，由于 Petri網(wǎng)以形式語言作為基礎(chǔ)，可形式化地對通信協(xié)議進行正確性驗證。隨著計算機網(wǎng)絡(luò)技術(shù)和信息

3、技術(shù)的發(fā)展，對網(wǎng)絡(luò)進行性能分析的需要，不僅出現(xiàn)于企業(yè)內(nèi)部的生產(chǎn)控制的局域總線網(wǎng)，而且出現(xiàn)于光纖局域網(wǎng)或ATM網(wǎng)中。圖1.1 Petri 網(wǎng)基本模型 由于產(chǎn)品開發(fā)中的競爭和革新需要，導(dǎo)致產(chǎn)品開發(fā)者面臨巨大壓力。在軟件工程中Petri網(wǎng)主要用于軟件系統(tǒng)的建模和分析，比較成熟的是加色Petri網(wǎng)，可以用于大型軟件系統(tǒng)的設(shè)計、說明、仿真、確認和實現(xiàn)，在軟件開發(fā)生命周期的各個階段，Petri網(wǎng)都可以得到很好的應(yīng)用。Petri網(wǎng)可用于Al中的知識表達和推理的形式化模型的建立，可以表達各個活動之間的各種關(guān)系，如順序關(guān)系、與關(guān)系、或關(guān)系等，并可在模型基礎(chǔ)上通過已知的初始狀態(tài)和初始條件進行邏輯推理。柔性制造系統(tǒng)

4、(FMS)對于現(xiàn)代制造業(yè)具有重要作用，Petri網(wǎng)由于其自身優(yōu)點，在制造系統(tǒng)中應(yīng)用廣泛，如帶緩沖區(qū)的簡單生產(chǎn)線、機床加工中心、自動生產(chǎn)線、柔性制造系統(tǒng)和及時加工系統(tǒng)。系統(tǒng)的可靠性不僅包括硬件的可靠性、也包括軟件可靠性.利用隨機Petri網(wǎng)對系統(tǒng)進行可靠性分析，對軟件復(fù)用、軟件可靠性分析。Petri 網(wǎng)描述系統(tǒng)的最基本概念是庫所和變遷。庫所表示系統(tǒng)的狀態(tài)。變遷表示資源的消耗、使用及使系統(tǒng)狀態(tài)產(chǎn)生的變化。變遷的發(fā)生受到系統(tǒng)狀態(tài)的控制，即變遷發(fā)生的前置條件必須滿足；變遷發(fā)生后，某些前置條件不再滿足，而某些后置條件則得到滿足。 庫所中令牌分布決定變遷的使能（enabled）和激發(fā)（fire），變遷的激

5、發(fā)又將改變令牌的分布。以變遷激發(fā)導(dǎo)致令牌在庫所間的流動，Petri網(wǎng)可以用于模擬系統(tǒng)的動態(tài)運行過程，反映系統(tǒng)的動態(tài)特性。網(wǎng)N=（P，T；F）構(gòu)成了描述系統(tǒng)靜態(tài)結(jié)構(gòu)框架，但還不能描述系統(tǒng)靜態(tài)結(jié)構(gòu)的全貌。網(wǎng)論尊重資源有限的事實。實際上，變遷發(fā)生所需的資源是有 限的，庫所容量也應(yīng)是有限的。完整的網(wǎng)系統(tǒng)應(yīng)指明資源的初始分布，規(guī)定變遷的活動原則，確定庫所容量和變遷與資源數(shù)量之間的關(guān)系。2 擴展 Petri 網(wǎng)的研究2.1 擴展的 Petri 網(wǎng)在以 Petri 網(wǎng)為工具對特定的系統(tǒng)進行建模分析時，不僅要遵守嚴格的語義還要兼顧圖形語言。用 Petri 網(wǎng)建立的模型可能十分的復(fù)雜，因為在一個動態(tài)的網(wǎng)絡(luò)圖中很

6、多活動都需要用一個庫所、一個變遷以及連接它們的一條連接弧來表示。如果系統(tǒng)中處于動態(tài)過程的活動過多，利用 Petri 網(wǎng)對其建立模型會產(chǎn)生狀態(tài)爆炸的現(xiàn)象。由于 Petri網(wǎng)在設(shè)計之初并沒有引入層次化的建模理念，這導(dǎo)致了利用 Petri 網(wǎng)建立的工作流模型很難重復(fù)利用，難以進行有效維護，理解起來非常困難。區(qū)別于傳統(tǒng)的面向問題的方法的面向?qū)ο蠓椒?，使得計算機能以更加類似人類的思維方式解決問題，從而直觀地描述客觀世界，并擁有封裝性、繼承性、支持軟件的復(fù)用以及易于擴充等優(yōu)點。在 Aalst提出的工作流網(wǎng)的基礎(chǔ)上引入對象技術(shù)及細化變遷實現(xiàn)流程的分層建模，可以降低建模的復(fù)雜程度，提高模型的可讀性和重用性。從

7、系統(tǒng)建模角度，將板材加工FMS中的活動分為三類： 以沖壓和剪切為特征的沖剪操作； 沖剪后零件的折彎操作； 板料以及沖剪后零件的出入庫操作。采用Petri網(wǎng)建模的基本步驟： 劃分和定義系統(tǒng)內(nèi)所有活動及其相互關(guān)系； 采用Petri網(wǎng)描述上述活動及其關(guān)系，得到系統(tǒng)Petri網(wǎng)模型。2.2 Petri網(wǎng)的行為特性與其它建模方法相比，Petri網(wǎng)的優(yōu)點不僅表現(xiàn)在建模能力上，更主要表現(xiàn)在它所具有的分析能力上。Petri網(wǎng)具有一些專門的分析手段，對系統(tǒng)活性（liveness）及死鎖（deadlock）進行分析，分析系統(tǒng)中的順序、并發(fā)及沖突等復(fù)雜事件關(guān)系。采用可達樹（reachability tree）理論分

8、析系統(tǒng)的有界性（boundness）與安全性（safety）等。Petri網(wǎng)的可達性是研究任何系統(tǒng)動態(tài)特性的基礎(chǔ),決定系統(tǒng)能否到達一個指定的狀態(tài)。 (1)系統(tǒng)按照一定的流程運行，系統(tǒng)是否能夠?qū)崿F(xiàn)一定的狀態(tài)；或者不期望的狀態(tài)不出現(xiàn)。比如：生產(chǎn)調(diào)度計劃的驗證（按照一定的生產(chǎn)調(diào)度計劃進行生產(chǎn)，一定的生產(chǎn)任務(wù)是否能夠完成）（2）要求到達一定的狀態(tài)，如何確定系統(tǒng)的運行軌跡（流程）。比如：生產(chǎn)調(diào)度，如何安排作業(yè)順序？活性在系統(tǒng)中用于檢測是否存在死鎖。一個系統(tǒng)存在的一個潛在問題是死鎖,為了避免死鎖,系統(tǒng)的Petri網(wǎng)模型必須具有活性。（1）互斥：同時爭奪唯一資源（2）占用且等待（3）無搶占（4）循環(huán)等待有界

9、性是一個非常重要的特性，它保證系統(tǒng)在運行過程中不會需要無限的資源。有界性反映一個庫所在系統(tǒng)運行過程中能夠獲得的最大的令牌數(shù)，即所能獲得的最大資源數(shù)，它與系統(tǒng)的初始令牌有關(guān)。在實際系統(tǒng)設(shè)計中，必須使網(wǎng)絡(luò)中的每個庫所在任何狀態(tài)下的令牌數(shù)小于庫所的容量，這樣才能保證系統(tǒng)的正常運行。2.3 擴展 Petri 網(wǎng)的觸發(fā)機制擴展的 Petri 網(wǎng)能夠區(qū)別變遷的使能和變遷的實施兩種不同狀態(tài)。被使能的變遷如果要得以真正實施，必須滿足一定的條件即具備相應(yīng)的觸發(fā)機制。使被使能的變遷真正實施的外部條件即為觸發(fā)機制，它主要由以下 4 種類型：第一，自動觸發(fā)：變遷被使能的同時觸發(fā)，通常用于那些通過應(yīng)用程序來自動執(zhí)行、不

10、需要與人進行交互的自動型活動。第二，人工觸發(fā)：活動的執(zhí)行通過執(zhí)行者從工作流任務(wù)管理器提供的工作流任務(wù)表中選擇工作項來進行觸發(fā)。當執(zhí)行者選中某一工作項時，此工作項開始執(zhí)行，被轉(zhuǎn)換為活動。第三，消息觸發(fā)：由系統(tǒng)外部的消息(事件)來觸發(fā)，如 E-mail，EDI 消息的到來。第四，時間觸發(fā)：由控制時間的定時器來觸發(fā)。3 基于 Petri 網(wǎng)的工作流網(wǎng)研究作為一種良好的建模工具，如今 Petri 網(wǎng)已經(jīng)被廣泛地運用到很多方面。如數(shù)據(jù)分析、協(xié)議驗證、工作流管理、工作流模式、并行程序設(shè)計、軟件設(shè)計等。但是由于經(jīng)典 Petri 網(wǎng)存在沒有測試庫所中零令牌的能力、模型容易變得很龐大、模型不能反映時間方面的內(nèi)容

11、、不支持構(gòu)造大規(guī)模模型如自頂向下或自底向上等局限性，在實際運用中需要對其進行改進。為了解決這些問題 Aalst 等人對經(jīng)典 Petri 網(wǎng)進行了擴展和改進，定義了工作流網(wǎng)(Workflow net，WF-net)模型及其有效性準則，采用了任務(wù)對應(yīng)變遷、狀態(tài)對應(yīng)庫所的策略，孤立地定義了單個案例的動態(tài)行為。當用 WFN 對工作流模型進行描述時，庫所用的圓圈表示條件，有兩方面的作用：確保任務(wù)按正確的次序執(zhí)行；用來表示案例的狀態(tài)。而變遷節(jié)點用的矩形表示工作流任務(wù)。庫所到變遷或變遷到庫所間的弧表示任務(wù)和工作流的邏輯關(guān)聯(lián)形式。庫所中包含的黑點(托肯)表示工作流執(zhí)行的狀態(tài)。只有每個輸入庫所至少有一個托肯，變

12、遷才能夠?qū)嵤９ぷ髁骶W(wǎng)模型中的任務(wù)包括順序、并行、選擇和循環(huán)四種路由結(jié)構(gòu)。工作流執(zhí)行的基本結(jié)構(gòu)由這四種路由構(gòu)成。這四種路由結(jié)構(gòu)按照一定的方式組合可以合成工作流所有的執(zhí)行結(jié)構(gòu)。為方便四種路由結(jié)構(gòu)的 Petri 網(wǎng)表示，引入與分叉、與合并、或分叉、或合并四種構(gòu)造模塊。與分叉和與合并的共同使用表示了一個并行執(zhí)行過程，或分叉和或合并的共同使用表示了一個選擇執(zhí)行過程。4 Petri 網(wǎng)模型的化簡規(guī)則化簡技術(shù)也稱歸約技術(shù)或模型轉(zhuǎn)換技術(shù)，它是以保證模型的基本特點為前提將過程模型化簡到適當?shù)某潭?，以方便對模型可能存在的各種沖突進行檢測。對擴展 Petri 網(wǎng)內(nèi)對象的化簡，首先可以在驗證合理性時將與工作流環(huán)境緊

13、密相關(guān)的觸發(fā)機制和工作流路由去掉。對于觸發(fā)機制只是簡單地忽略掉就可以了，而對于工作流路由的處理要復(fù)雜一些，需要把 OR-split、OR-join、AND-split、AND-join 這樣的工作流元組件還原成經(jīng)典 Petri 網(wǎng)中普通的庫所和變遷，這樣新生成的模型中不再有專門的控制變遷。5 Petri 網(wǎng)模型的正確性分析工作流過程定義結(jié)束后，需要對其進行正確性驗證，只有在證明了所建工作流模型無死鎖、無死任務(wù)，是合理的、安全的之后，對其進行性能分析、仿真優(yōu)化才有意義。工作流的正確性對業(yè)務(wù)過程目標的正確完成有著重要的影響。工作流模型的正確性包括兩方面的含義：結(jié)構(gòu)上的正確性(即工作流模型是安全的、

14、無死鎖的)和語義上的正確性(即在完成業(yè)務(wù)目標上是與實際業(yè)務(wù)過程等價的)。對工作流模型的正確性分析主要指對工作流模型結(jié)構(gòu)上的正確性進行分析。目前，在模型的正確性研究方面，主要有以下兩種方法：可達圖分析和化簡。利用 Petri 網(wǎng)可達圖分析技術(shù)分析結(jié)點較多的模型時，尤其是集成制造領(lǐng)域的模型，其過程會很復(fù)雜，驗證所需的時間隨節(jié)點個數(shù)呈指數(shù)增長會導(dǎo)致狀態(tài)空間爆炸；而且可達圖分析技術(shù)只能提供模型正確與否的結(jié)論，而無法具體地定位錯誤，不便輔助設(shè)計者修改模型。6 Petri 網(wǎng)的步語義問題Petri 網(wǎng)的步語義（step semantics）是一種有效的建模方法，它與順序語義（sequence semant

15、ics）相比對實際行為的描述更為詳盡，而與難以掌握的偏序技術(shù)相比更貼近實際，是順序語義與偏序技術(shù)在實用性和表達能力上的折衷。Philippe Darondeau 等人針對步語義可能引起狀態(tài)爆炸以及缺乏對行為協(xié)調(diào)有效支持兩個缺點，引入了步觸發(fā)策略，它限制了 Petri 網(wǎng)并發(fā)行為，因此改進了步語義的執(zhí)行和建模特征。Matthias Jantzen 等人比較了各種變遷觸發(fā)方式，定義了 Petri 網(wǎng)中通過步、最大步、多步和最大多步語義生成的語言；通過允許在一個多步中多次使用變遷，得到一個語言體系，彌補了帶標記 Petri 網(wǎng)步語義所定義的語言在若干方面的缺失。7 Petri 網(wǎng)的合成Petri 網(wǎng)

16、的合成自 20 世紀 90 年代起逐漸成為本領(lǐng)域內(nèi)一個研究熱點，它探討如何從系統(tǒng)的一個行為規(guī)范描述生成一個行為等價 Petri 網(wǎng)模型。 J. Carmona 等人提出了一個從變遷系統(tǒng)生成有界 Petri網(wǎng)的算法，這個算法基于一般域（general region）的理論將已有的 Petri 網(wǎng)合成算法由安全網(wǎng)擴展到有界網(wǎng)，根據(jù)這一擴展，合成算法的適用范圍擴大到帶有權(quán)弧的 k-階 Petri 網(wǎng)。而且這個合成算法使用基于 BDD 的符合化表示方法來表達狀態(tài)空間，從而有效地生成最小域，與安全網(wǎng)的合成方法相比，生成的網(wǎng)模型更簡單直觀。通過研究有步觸發(fā)策略的 Petri 網(wǎng)合成方法，給出一個公理，說明

17、一個變遷系統(tǒng)在何種條件下能夠由一個給定步進觸發(fā)策略控制的 Petri 網(wǎng)的可達圖來表示。 J.M.E.M. vander Werf 等人給出了一種基于域理論的流程發(fā)掘算法，由系統(tǒng)的執(zhí)行日志生成 Petri 網(wǎng)模型。域理論起源于硬件設(shè)計控制領(lǐng)域，用于由行為說明構(gòu)造 Petri 網(wǎng)。由于域理論直接應(yīng)用于流程發(fā)掘會導(dǎo)致生成的網(wǎng)模型中庫所個數(shù)依賴于日志規(guī)模，作者通過引入整數(shù)線性規(guī)劃思想，由庫所來限制網(wǎng)的可能觸發(fā)序列，解決了這個問題。 在展示工具的論文中，也有一篇是關(guān)于 Petri 網(wǎng)合成的：Robin Bergenthum 等人展示了一個由場景合成 Petri 網(wǎng)的工具，它為基于 Petri 網(wǎng)的商業(yè)

18、流程工具 viptool 加入了 Petri 網(wǎng)合成的新特性，改寫了流程建模的起點，由用戶設(shè)計流程的合適場景，再根據(jù) Petri 網(wǎng)合成工具生成流程模型。8 Petri 網(wǎng)的網(wǎng)展開網(wǎng)展開技術(shù)是一種 Petri 網(wǎng)的狀態(tài)空間搜索方法，它通過構(gòu)造網(wǎng)的展開圖來進行各種離散事件系統(tǒng)的屬性分析。 Robin Bergenthum 等人針對標準的基于分支進程的網(wǎng)展開技術(shù)包含較多冗余的缺點，提出了兩種新的網(wǎng)展開語義，其中一個避免了同構(gòu)進程的出現(xiàn)，另一個減少了在底層運行時同構(gòu)的進程的個數(shù)。而且兩種新的展開圖模型仍然表達了完整的偏序行為。文中還給出兩種新模型的構(gòu)造算法，能夠快速生成規(guī)模小得多的展開圖模型。在上文

19、討論模型檢測時提到的論文5中，驗證移動系統(tǒng)采用的方法就是基于網(wǎng)展開的模型檢測技術(shù)。9 其他 Petri 網(wǎng)相關(guān)理論研究論文的研究對象是持續(xù)網(wǎng)（persistent Petri nets），它是比無沖突網(wǎng)（conflict-free nets）更一般的一類網(wǎng)模型，Eike Best 等人針對持續(xù)網(wǎng)早期理論引出的開放性問題進行了研究，使得構(gòu)造理論更貼近于持續(xù)網(wǎng)。還給出了這樣的結(jié)果：對于有界可逆的持續(xù)網(wǎng)，可達圖中的環(huán)能夠分解為更小的、不相交的環(huán)。這個結(jié)論縮小了網(wǎng)的線性代數(shù)性質(zhì)與更多組合性質(zhì)間的鴻溝。Kunihiko Hiraishi 基于連續(xù) Petri 模型使用狀態(tài)空間搜索方法分析了信息系統(tǒng)工作流

20、的性能。文中提出了一種新的連續(xù) Petri 網(wǎng)路由時間連續(xù) Petri 網(wǎng) RTCPN，用于近似一般化隨機 Petri 網(wǎng) GSPN 的離散狀態(tài)空間，并將這個新的網(wǎng)模型用于工作流數(shù)量性能的分析上，結(jié)果顯示新模型不受工作流實例個數(shù)的限制，擴展性更強。Ryszard Janicki 等人提出了一種新的建模理論，使用商半群來進行并發(fā)的建模。10 模型檢測研究Guy Edward Gallasch 等人討論了參數(shù)化系統(tǒng)的模型檢測問題。文章以 SWP （Stop-and-Wait）這類協(xié)議為對象，研究了帶有兩個無界參數(shù)的 SWP 模型檢測問題。以 SWP 的著色 Petri 網(wǎng) CPN 模型為基礎(chǔ)，構(gòu)造

21、了含有兩個參數(shù)的代數(shù)公式來符號化地表示相應(yīng)的可達圖的無窮族類，然后從代數(shù)表達式生成一個參數(shù)化的有限狀態(tài)自動機（FSA）來表達所有用戶可觀察的事件序列，再將其化簡得到一個簡單無參數(shù)的 FSA，最后通過比較 FSA 與表達用戶期待行為的服務(wù)語言的相等性來驗證 SWP 是否滿足預(yù)期性質(zhì)。Alexandre Hamez 等人研究了決策圖的模型檢測問題。狀態(tài)空間的共享決策圖能夠緩解大規(guī)模系統(tǒng)的狀態(tài)空間爆炸問題，但是變量的順序以及變遷關(guān)系定義和應(yīng)用方式會很大程度上影響性能。文中提出了一種分層決策圖優(yōu)化技術(shù)SDD（Hierarchical Set Decision Diagrams)，這個數(shù)據(jù)結(jié)構(gòu)提供了一種

22、有效的編碼結(jié)構(gòu)化規(guī)范方法，能夠應(yīng)付大型系統(tǒng)的復(fù)雜度。SDD 的能力還包括：根據(jù)少量的用戶輸入來優(yōu)化變遷關(guān)系的賦值，由此自動生成 Saturation（一種能有效解決決策圖技術(shù)中問題的方法）；允許用戶自由定義變遷關(guān)系。Kais Klai 等人設(shè)計了一個基于狀態(tài)符號化觀察圖（symbolic observation graph，SOG）的 On-the-fly 模型檢測器 MC-SOG，用于驗證有窮模型上基于狀態(tài)的 LTLX 性質(zhì)。On-the-fly 允許只生成與驗證屬性相關(guān)的部分模型，符號化模型檢測則是在一個使用二元決策圖（Binary Decision Diagram, BDD）技術(shù)系統(tǒng)的緊

23、湊表示上驗證屬性，文中的方法結(jié)合了這兩種技術(shù)，在檢測過程中生成系統(tǒng)狀態(tài)空間的抽象 SOG，其生成過程由待驗證的屬性指導(dǎo)，然后通過判斷 SOG 對 LTLX 公式的滿足性來驗證系統(tǒng)。這個檢測器已被實現(xiàn)在由 Petri 網(wǎng)建模的系統(tǒng)上。Morgan Magnin 等人研究了一種帶秒表的有界 Petri 網(wǎng) SwPNs（bounded Petri nets with stopwatches），提出一個符號化的方法，采用通常用于稠密時間的技術(shù)來計算帶秒表的離散時間 Petri 網(wǎng) SwPNs 的狀態(tài)空間，用于驗證系統(tǒng)的定時屬性，并給出這個模型的 TCTL 模型檢測算法。文中還證明了在特定情況下，通過簡

24、單地離散化相關(guān)的稠密時間網(wǎng)的狀態(tài)空間能夠計算出一個離散時間網(wǎng)的狀態(tài)空間。Roland Meyer 等人將基于網(wǎng)展開的安全 Petri 網(wǎng)模型檢測技術(shù)應(yīng)用于移動系統(tǒng)的驗證。首先，由 Pi 演算的一個著名子集 FCP（finite control process）建模移動系統(tǒng)，然后將 FCP 轉(zhuǎn)化為一個安全進程（safe process），進而轉(zhuǎn)化為安全網(wǎng)，再進行基于網(wǎng)展開的模型檢測。實驗結(jié)果顯示在內(nèi)存消耗和運行時間方面，此方法有明顯優(yōu)勢。11 Petri 網(wǎng)應(yīng)用Roland Bouroulet 等人介紹了一個構(gòu)架，用于描述和驗證全協(xié)議的屬性。此框架使得在分析協(xié)議時必須的隱式信息變成顯式、結(jié)構(gòu)化和

25、形式化的信息。首先將協(xié)議代理形式化為角色，然后將角色和可能與角色交互的環(huán)境都用 SPL（Security Protocol Language）進程表示，再將其轉(zhuǎn)化為高階 Petri 網(wǎng)，初始標識由協(xié)議中的上下文生成。這樣，Petri網(wǎng)的仿真與模型檢測技術(shù)就能用于協(xié)議屬性的分析和驗證。 Lay G. Ding 等人利用 CPN 建模和分析了一個面向事務(wù)的用于在 Internet 上初始化、修改和終止多媒體會話的控制協(xié)議 SIP（Session Initiation Protocol）。文章主要分析和驗證了在一個可靠傳輸介質(zhì)上進行的INVIFE事務(wù)，為INVITE創(chuàng)建了一個 CPN 模型，通過 C

26、PN 的狀態(tài)空間分析方法驗證了 INVIEF 的常規(guī)屬性，發(fā)現(xiàn)了一個非預(yù)期的行為，并據(jù)此對它進行了一些改動。 Kristian L. Espensen 等人應(yīng)用 CPN 模型和分析工具建模和驗證了一個路由協(xié)議 DYMO（Dynamic MANET On-demand）。MANET 是一個由一組移動通信設(shè)備通過無線通信建立起來的移動即時網(wǎng)絡(luò)，而 DYMO 是 MANET 中的一個用于多跳數(shù)通信的路由協(xié)議。文中給出了 DYMO 協(xié)議的CPN 模型，并使用狀態(tài)空間搜索驗證協(xié)議的重要屬性，對正在開發(fā)中的協(xié)議版本產(chǎn)生了直接影響。 Paul Fleischer 等人應(yīng)用 CPN 建模和驗證了一個通信協(xié)議。

27、通用訪問網(wǎng)體系 GAN 中要用到 IPSec 協(xié)議和 Internet 核心交換協(xié)議 IKEv2 來提供訪問 IP 網(wǎng)絡(luò)的加密技術(shù)，而 GAN 規(guī)范中只粗略地描述了兩種協(xié)議的使用方法，所以文中根據(jù)一個描述IPSec和IKEv2如何在連接建立過程中被使用的詳細 GAN 場景，構(gòu)造了一個 CPN 模型來形式化地說明和驗證這個場景。 Hendrik Oberheid 等人實現(xiàn)了一個CPN模型來模擬空中交通控制中的潛在到達計劃進程。文中首次提出一個形式化建模協(xié)調(diào)到達管理進程的方法，利用 CPN 模型提供了一種直觀的方法來建模和分析順序計劃問題的綜合特性，目的是研究計劃編制系統(tǒng)的不同動態(tài)屬性，并由此來優(yōu)

28、化系統(tǒng)性能，改進系統(tǒng)安全。 Filippo Bonchi 等人說明了如何通過 Petri 網(wǎng)的行為等價性來判斷服務(wù)描述的正確性與可替代性問題。具體地，文中定義了用于表示 OWL-S 描述的 Web 服務(wù)的網(wǎng)模型 OCPR（Open Consume-Produce-Read）網(wǎng)，在此基礎(chǔ)上定義了一個適用于 OWL-S 的行為等價性概念，這樣就能夠回答一個服務(wù)描述是否等價于服務(wù)實現(xiàn)，以及一個子服務(wù)能否在不改變整個應(yīng)用行為的前提下被另一個子服務(wù)替換的問題。 第一，Petri 網(wǎng)因其圖形化與描述異步并發(fā)的能力，非常適用于通信協(xié)議的建模，而 Petri 網(wǎng)的多種分析方法與工具也給協(xié)議的分析和驗證提供了便

29、利；第二，著色 Petri 網(wǎng) CPN 作為一種高級網(wǎng)模型，它的狀態(tài)空間分析方法和支持工具已經(jīng)被廣泛應(yīng)用于驗證通信協(xié)議、軍用系統(tǒng)、商業(yè)流程、Web 服務(wù)應(yīng)用和其他各種軟件系統(tǒng)。12 Petri 網(wǎng)工具Lawrence Cabac 等人針對面向代理的軟件工程AOSE工具缺少系統(tǒng)的全局狀態(tài)監(jiān)測及動態(tài)操作環(huán)境的問題，提出了兩個結(jié)合 AOSE 范式與 Petri 網(wǎng)表達能力的 PAOSE 工具MULAN-Viewer 和 MULAN-Sniffer，用于處理在調(diào)試、監(jiān)測及測試代理應(yīng)用時遇到的問題。Joao Lourenco 等人提出了一個生成監(jiān)測特定進程的圖形化用戶接口的自動化設(shè)計工具。當前對于離散事

30、件建模，特別是 Petri 網(wǎng)，很難找到完全支持代碼生成和動畫式交互的圖形用戶接口及 SCADA（監(jiān)督、控制、數(shù)據(jù)獲取系統(tǒng)）工具，作者針對這個問題實現(xiàn)了一個自動化工具，它能夠自動生成一個中心化的 SCADA 系統(tǒng)，實現(xiàn)了以 Petri 網(wǎng)為行為模型、基于本地圖形化用戶接口的進程控制器執(zhí)行監(jiān)督和控制的機制。 Fausto Sessego 等人實現(xiàn)了一個開源工具 HYPENS，用于仿真離散時間、連續(xù)時間以及混合 Petri 網(wǎng)，它在 Matlab中開發(fā)，允許用戶和設(shè)計者利用已經(jīng)在 Matlab 中事先定義的功能和結(jié)構(gòu)。13 Petri網(wǎng)會議第 29 屆 Petri 網(wǎng)應(yīng)用與理論及其他并發(fā)模型國際會議（29th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, 簡稱 PETRI NETS 2008）于 2008 年 6 月 23 至 27 日在西安召開。該會是國際 Petri 網(wǎng)研究領(lǐng)域最高水平和最富影響力的學(xué)術(shù)會議，起始于 1980 年，當時稱為歐洲 Pet