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

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

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

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

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

5、發(fā)又將改變令牌的分布。以變遷激發(fā)導(dǎo)致令牌在庫(kù)所間的流動(dòng)，Petri網(wǎng)可以用于模擬系統(tǒng)的動(dòng)態(tài)運(yùn)行過(guò)程，反映系統(tǒng)的動(dò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)論尊重資源有限的事實(shí)。實(shí)際上，變遷發(fā)生所需的資源是有 限的，庫(kù)所容量也應(yīng)是有限的。完整的網(wǎng)系統(tǒng)應(yīng)指明資源的初始分布，規(guī)定變遷的活動(dòng)原則，確定庫(kù)所容量和變遷與資源數(shù)量之間的關(guān)系。2 擴(kuò)展 Petri 網(wǎng)的研究2.1 擴(kuò)展的 Petri 網(wǎng)在以 Petri 網(wǎng)為工具對(duì)特定的系統(tǒng)進(jìn)行建模分析時(shí)，不僅要遵守嚴(yán)格的語(yǔ)義還要兼顧圖形語(yǔ)言。用 Petri 網(wǎng)建立的模型可能十分的復(fù)雜，因?yàn)樵谝粋€(gè)動(dòng)態(tài)的網(wǎng)絡(luò)圖中很

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

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

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

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

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

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

12、遷才能夠?qū)嵤?。工作流網(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)造模塊。與分叉和與合并的共同使用表示了一個(gè)并行執(zhí)行過(guò)程，或分叉和或合并的共同使用表示了一個(gè)選擇執(zhí)行過(guò)程。4 Petri 網(wǎng)模型的化簡(jiǎn)規(guī)則化簡(jiǎn)技術(shù)也稱歸約技術(shù)或模型轉(zhuǎn)換技術(shù)，它是以保證模型的基本特點(diǎn)為前提將過(guò)程模型化簡(jiǎn)到適當(dāng)?shù)某潭龋苑奖銓?duì)模型可能存在的各種沖突進(jìn)行檢測(cè)。對(duì)擴(kuò)展 Petri 網(wǎng)內(nèi)對(duì)象的化簡(jiǎn)，首先可以在驗(yàn)證合理性時(shí)將與工作流環(huán)境緊

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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