需要其他书籍此网站未展示的，请加微信（bookbook66）咨询。

说明：本站只收集整理市场上难买的绝版书籍，方便科研人员查阅！为保护版权，请在使用后自觉删除。

《形式化方法导论》是由12章构成，主要论述有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动的书籍。

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

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

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

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