形式化方法是指有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动。随着软件可信需求的不断增长，形式化方法的重要性和关注度日益提高。 本书共12章，第1章概述形式化方法，第2章介绍形式化方法发展早期的经典内容，其余部分共分3篇： 上篇（第3～5章）为系统建模篇，着重介绍迁移系统、有穷自动机、Petri网等基本计算模型； 中篇（第6和第7章）为形式规约篇，着重讨论时序逻辑及其在并发系统属性描述的应用； 下篇（第8～12章）为形式验证篇，着重介绍定理证明方法和并发、实时及混成系统的各种模型检测方法及相关验证工具。全书提供了大量应用实例，每章后均附有习题。 本书适合作为高等院校计算机、软件工程、人工智能、网络工程、信息安全、自动化等专业高年级本科生、研究生的教材，同时可供相关领域的研究人员和技术开发人员参考。

张广泉,苏州大学教授、工学博士，中国科学院计算机科学国家重点实验室博士后。师从我国计算机科学和软件工程领域先驱和开拓者之一、国家自然科学一等奖及何梁何利奖获得者、中国科学院院士唐稚松先生。2002年任教授，曾任计算机教研室主任(1991-1996)、苏州大学软件工程系主任(2004-2009)，现任全国高校计算机教育研究会理事、信息技术新工科产学研联盟会员单位负责人、中国计算机学会教育专委委员、软件工程、系统软件、形式化方法等专委委员、江苏省计算机软件科技传播专家、江苏省计算机软件与教育专委委员等。

第2版前言 近年来，形式化方法的一个重要内容——基于定理证明的形式验证方法取得了较大进展和突破。一方面，随着自动证明理论的发展和计算机处理器能力的大幅增强，基于自动定理证明器的自动验证能力大幅提升，如微软公司开发的SMT求解器Z3已成为目前使用最广泛的自动定理证明器； 另一方面，基于人机交互的半自动证明在可验证的系统软件上取得显著突破，如分别在交互式定理证明器Coq和Isabelle/HOL的支持下，INRIA对C语言编译器CompCert的验证及NICTA对操作系统微内核seL4的验证等。 本次修订除更正第1版的一些文字及印刷错误和叙述不当之处外，主要修订第8章及与之关联的部分章节内容，重点阐述了一些典型的定理证明方法、工具和应用。此外，还补充介绍了我国科学家在形式化方法领域的部分开创性研究工作。 　　本书修订工作得到江苏省高等学校重点教材立项建设、江苏高校优势学科建设工程项目资助和江苏省计算机学会立项资助，以及苏州大学教务处和计算机科学与技术学院的关心和支持，中国科学院软件研究所晏荣杰副研究员对本书修订提出了宝贵的建议，清华大学出版社安妮编辑为本书再版做了大量工作，在此一并表示诚挚的感谢。 张广泉 2023年1月于苏州大学天赐庄校区 第1版前言 软件产业是信息产业的核心，是国家信息化的基础和支撑。软件是工业4.0和中国制造2025的使能和驱动。为推进产业结构优化升级，加快培养软件人才的步伐，近年来教育部大力发展高校软件工程教育，软件工程已从最初的计算机科学与技术的一个学科方向调整为包括...