本书是一本关于Petri网的建模、验证与应用的优秀的教学与研究参考书。全书分为5个部分共27章,首先讲解了Petri网的基本概念,通过实例介绍了常量弧网、库所/变迁网和有色网的基本定义。作者接着讨论了如何应用Petri网来构造系统,并给出了各种建模的方法。书中介绍了对Petri网模型进行验证的主要方法,其中包括基于状态空间的方法和模型检验、结构方法以及使用演绎和进程代数的一些高级方法;讲解了Petri网的确认和执行,其中不仅涉及到软件生命周期的相关内容,而且详细介绍了在复杂系统的开发过程中如何使用Petri网进行建模和分析。最后,作者对Petri网的三个不同应用领域(柔性制造系统、工作流管理系统和电信系统)进行了深入的研究。本书的内容全面,结构清晰,并通过大量实例讲解了各种概念、方法与应用。本书可以作为计算机相关专业本科生和研究生的教材或参考书,也可作为从事软件系统研究的人员的宝贵参考资料。越来越大、越来越复杂的系统,使得应用在硬件和软件的规范与验证中的形式化方法越来越重要。本书旨在通过Petri网的形式化过程来阐述形式化方法中的相关进展。书中采用了许多实例,它们来源于不同的应用领域,例如柔性制造系统、工作流管理系统和电信系统。本书的内容涵盖了一个系统在设计和实现的整个生命周期中的几个主要阶段,即规范、用于证明的模型验证技术、性质分析、代码生成和模型的执行。书中对这些技术及其支持工具进行了详细的讨论,并且分析了在实际应用中可能遇到的问题。除此之外,作者还系统地介绍了一些基本概念,例如组合、抽象、模型复用、模型验证、性质验证等。