第2版前言


近年来，形式化方法的一个重要内容——基于定理证明的形式验证方法取得了较大进展和突破。一方面，随着自动证明理论的发展和计算机处理器能力的大幅增强，基于自动定理证明器的自动验证能力大幅提升，如微软公司开发的SMT求解器Z3已成为目前使用最广泛的自动定理证明器； 另一方面，基于人机交互的半自动证明在可验证的系统软件上取得显著突破，如分别在交互式定理证明器Coq和Isabelle/HOL的支持下，INRIA对C语言编译器CompCert的验证及NICTA对操作系统微内核seL4的验证等。

本次修订除更正第1版的一些文字及印刷错误和叙述不当之处外，主要修订第8章及与之关联的部分章节内容，重点阐述了一些典型的定理证明方法、工具和应用。此外，还补充介绍了我国科学家在形式化方法领域的部分开创性研究工作。

　　本书修订工作得到江苏省高等学校重点教材立项建设、江苏高校优势学科建设工程项目资助和江苏省计算机学会立项资助，以及苏州大学教务处和计算机科学与技术学院的关心和支持，中国科学院软件研究所晏荣杰副研究员对本书修订提出了宝贵的建议，清华大学出版社安妮编辑为本书再版做了大量工作，在此一并表示诚挚的感谢。


张广泉
2023年1月于苏州大学天赐庄校区







第1版前言



软件产业是信息产业的核心，是国家信息化的基础和支撑。软件是工业4.0和中国制造2025的使能和驱动。为推进产业结构优化升级，加快培养软件人才的步伐，近年来教育部大力发展高校软件工程教育，软件工程已从最初的计算机科学与技术的一个学科方向调整为包括软件工程理论与方法、软件工程技术、软件服务工程和领域软件工程等学科方向的、独立的一级学科。软件工程理论与方法是软件工程一级学科的基础，作为其核心内容之一，形式化方法是指有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动。随着软件可信需求的不断增长，形式化方法的重要性和关注度日益提高。

形式化方法相关的教学工作已经得到欧美国家高等学校的重视和推广，知识体系和课程教学内容日趋完善。而目前国内高校关于形式化方法教育还相对薄弱，主要因素之一是缺乏比较全面、系统介绍形式化理论、方法和应用的教材。

本书是在学习、总结形式化方法领域国内外相关文献的基础上，结合作者多年从事形式化方法教学和科研的实践撰写而成的，本书具有以下几个特点： 

（1） 通过详细分析和梳理，提炼出形式化方法核心、本质的原理、方法和技术，其中自动机和时序逻辑是贯穿全书内容的两大重要基础。

（2） 重点阐述以模型检测为主要内容的形式化验证方法，使学生在有限的学时范围内，能有效地掌握形式化方法自动化部分的核心内容。

（3） 注重实践与应用，详细介绍SPIN、UPPAAL和PRISM等典型的形式化验证工具的使用方法，结合实例分析，达到理论学习与实际应用的有机结合。

全书共12章。其中第1章概述形式化方法的发展历程和基本内容，第2章介绍形式化方法发展早期的经典内容，即串行程序的正确性证明。其余部分针对并发系统，分为上、中、下三篇阐述形式化建模、规约和验证方法。其中： 

上篇（第3～5章）为系统建模篇，主要介绍三个典型的并发系统计算模型。第3章介绍基于状态迁移的计算模型——迁移系统，第4章介绍描述有穷状态系统的计算模型——有穷自动机，它也是计算机科学中最基本的数学模型，第5章介绍最早的并发计算模型——Petri网。

中篇（第6和第7章）为形式规约篇，着重讨论并发系统属性的主要规约方法及应用。第6章介绍真假值依赖时间而变化的非经典逻辑——时序逻辑，它是描述并发系统属性的重要工具，第7章重点阐述并发系统最基本的两类属性——安全性和活性，及其时序逻辑描述方法。

下篇（第8～12章）为形式验证篇，着重介绍主要的形式验证方法及相关验证工具。第8章介绍基于时序逻辑的演绎证明方法及验证工具STeP，第9~12章重点阐述模型检测方法、工具及其在并发、实时及混成系统中的应用，这是形式化方法自动化的核心内容，也是本书的重点。其中第9章介绍经典的模型检测算法、验证工具SPIN及应用，第10章介绍基于二叉判定图(BDD)的符号模型检测方法、验证工具SMV及应用，第11章介绍模型检测与概率分析方法相结合的概率模型检测方法、验证工具PRISM及应用，第12章介绍实时与混成系统的模型检测方法、验证工具UPPAAL及应用。

全书提供了大量应用实例，每章后均附有习题。

本书由张广泉担任主编，负责全书内容的组稿、统稿和修改工作。顾玉磊、宋相君、宋振华、项周坤、沈兴勤、郑林峰、张红美等参与了书稿整理、文字录入和校对工作，祝义副教授、孙庆英老师、魏慧老师等参与了部分书稿的校对工作，在此对他们的辛勤劳动表示感谢。此外，在本书的编写过程中，参考了大量国内外相关文献，在此对本书所引用文献的作者深表感谢。

本书编写工作得到江苏省“十二五”高等学校重点教材立项建设和苏州大学教材培育项目的资助，以及江苏省自然科学基金（BK2011281）、中国科学院软件研究所计算机科学国家重点实验室开放课题（SYSKF0908、SYSKF1201）、南京大学计算机软件新技术国家重点实验室开放课题（KFKT2012B15）的支持和帮助。中国科学院软件研究所焦莉研究员、李广元副研究员、朱雪阳博士、晏荣杰博士仔细阅读了本书初稿，提出了许多重要的修改意见与建议，在此表示衷心感谢。本书的编写还得到中国科学院软件研究所周巢尘院士、林惠民院士、沈一栋研究员、张健研究员、张文辉研究员、詹乃军研究员、南京大学李宣东教授、上海大学缪淮扣教授、南京航空航天大学黄志球教授、东南大学李必信教授等及苏州大学教务部和计算机科学与技术学院的关心和支持，清华大学出版社黄芝和薛阳编辑为本书出版做了大量工作，在此一并表示诚挚的感谢。

由于编者水平有限，书中难免有不当之处，敬请读者批评指正。


张广泉
2015年10月于苏州大学天赐庄校区