本書是一本關于Petri網的建模、驗證與應用的優(yōu)秀的教學與研究參考書。全書分為5個部分共27章,首先講解了Petri網的基本概念,通過實例介紹了常量弧網、庫所/變遷網和有色網的基本定義。作者接著討論了如何應用Petri網來構造系統,并給出了各種建模的方法。書中介紹了對Petri網模型進行驗證的主要方法,其中包括基于狀態(tài)空間的方法和模型檢驗、結構方法以及使用演繹和進程代數的一些高級方法;講解了Petri網的確認和執(zhí)行,其中不僅涉及到軟件生命周期的相關內容,而且詳細介紹了在復雜系統的開發(fā)過程中如何使用Petri網進行建模和分析。最后,作者對Petri網的三個不同應用領域(柔性制造系統、工作流管理系統和電信系統)進行了深入的研究。本書的內容全面,結構清晰,并通過大量實例講解了各種概念、方法與應用。本書可以作為計算機相關專業(yè)本科生和研究生的教材或參考書,也可作為從事軟件系統研究的人員的寶貴參考資料。越來越大、越來越復雜的系統,使得應用在硬件和軟件的規(guī)范與驗證中的形式化方法越來越重要。本書旨在通過Petri網的形式化過程來闡述形式化方法中的相關進展。書中采用了許多實例,它們來源于不同的應用領域,例如柔性制造系統、工作流管理系統和電信系統。本書的內容涵蓋了一個系統在設計和實現的整個生命周期中的幾個主要階段,即規(guī)范、用于證明的模型驗證技術、性質分析、代碼生成和模型的執(zhí)行。書中對這些技術及其支持工具進行了詳細的討論,并且分析了在實際應用中可能遇到的問題。除此之外,作者還系統地介紹了一些基本概念,例如組合、抽象、模型復用、模型驗證、性質驗證等。