越来越大、越来越复杂的系统，使得应用在硬件和软件的规范与验证中的形式化方法越来越重要。本书旨在通过Petri网的形式化过程来阐述形式化方法中的相关进展。书中采用了许多实例，它们来源于不同的应用领域，例如柔性制造系统、工作流管理系统和电信系统。本书的内容涵盖了一个系统在设计和实现的整个生命周期中的几个主要阶段，即规范、用于证明的模型验证技术、性质分析、代码生成和模型的执行。书中对这些技术及其支持工具进行了详细的讨论，并且分析了在实际应用中可能遇到的问题。

本书是一本关于Petri网的建模、验证与应用的优秀的教学与研究参考书。全书分为5个部分共27章，首先讲解了Petri网的基本概念，通过实例介绍了常量弧网、库所／变迁网和有色网的基本定义。作者接着讨论了如何应用Petri网来构造系统，并给出了各种建模的方法。书中介绍了对Petri网模型进行验证的主要方法，其中包括基于状态空间的方法和模型检验、结构方法以及使用演绎和进程代数的一些高级方法；讲解了Petri网的确认和执行，其中不仅涉及到软件生命周期的相关内容，而且详细介绍了在复杂系统的开发过程中如何使用Petri网进行建模和分析。最后，作者对Petri网的三个不同应用领域(柔性制造亲统、工作流管理系统和电信系统)进行了深入的研究。本书的内容全面，结构清晰，并通过大量实例讲解了各种概念、方法与应用。  本书可以作为计算机相关专业本科生和研究生的教材或参考书，也可作为从事软件系统研究的人员的宝贵参考资料。

《系统工程Petri网——建模、验证与应用指南》一书是由法国、德国、荷兰和西班牙的24位专家集体创作而成。虽然本书的各个章节由不同的作者执笔，但是全书的结构和内容却是经他们在若干次会议上无数次讨论的结果。译者有幸认识其中的几位，并且熟悉或了解他们的工作。作为大学教授或科研人员，本书的各位作者都有着多年的教学实践和科研(特别是Petri网的应用研究)经验。经由这些作者撰写而成的一本书，无疑值得所有从事计算机应用(特别是软件工程)的人员阅读。

中文书名中的“系统”一词是指以计算机应用为背景的系统，因此将本书译为《软件工程Petri网》也无不可。这是一本由实例引入概念和方法的著作，其内容深入浅出，只要读者有一些计算机应用的实践经验以及一定的数学基础，就可以轻松地学习到Petri网的相关知识，学会使用Petri N进行建模，通过Petri网进行分析，以及学会抽象和形式化地处理应用问题。如果读者还不了解什么是Petri网，不知道为什么要学习和应用Petri网，不妨先阅读一下本书的前言和第一章。译者不想在这里重复作者对本书写作动机和目标的阐述，也不想通过介绍Petri网的很多特别之处(优点)来吸引读者；译者只想在这里指出阅读本书时可能会遇到的问题，希望有助于读者更快、更深入地理解本书的内容。

学习过代数理论的人都会知道，线性方程组中的变量只代表某个数值，只有在使用线性方程组解决应用问题时才将变量与问题中的物理对象联系起来。Petri网也是这样，在研究和学习Petri网时不需要了解构成Petri网的元素的物理含义。Petri网有它自己的一套体系和一套层次，并且有着相当完整的知识结构。本书只从实用的角度引入Petri网的概念和各种Petri网系统，通过实例来解释它们。这种方式的优点是直观、易于被读者接受；缺点是不太符合Petri网自身的体系，同时也欠缺深度。这里可能会出现的问题是，读者也许很容易理解各章的具体内容，但是却很难形成整体认识。译者的建议是，如果读者尚不了解Petri网，那么不妨先阅读一些以介绍Petri网为主要内容的著作或文章，例如本书的参考文献[Mur89]和[Pet81]，或者参阅译者的专著之一——《Petri网原理与应用》(即将由电子工业出版社于近期出版)。对于了解Petri网的一部分读者来说，如果在阅读完本书之后仍然不能完整和深入地掌握Petri网的概念与应用，那么也可以参考以上提及的文献或专著。[Mur89]和[Pet8l]都是很容易理解的入门教材，具有一定英文基础的读者都可以轻松地阅读。在本书的翻译过程中，我们为了统一风格，先将专有名词翻译出来，如将“marking”译为“标识”，将“token”译为“托肯”。某些技术名词在不同场合有不同的译法，例如“model”一词，我们根据不同的上下文将其翻译为“模型”、“建模”或“模拟”。还有一些术语在翻译时较难找到十分恰当的汉语词汇与之相对应，因此我们采用保留英文术语的方式，如“on-the-fly verification”直接翻译成“on-the-fly验证”。

 参加本书翻译工作的有霍金健(第一部分和第五部分)、余鹏(第二部分和第四部分）、王生原(第三部分)。最后，由袁崇义教授对全书的译文进行了校对和整理。由于译者的水平有限，文中难免有不妥之处，敬请读者不吝赐教。