本书全面系统地介绍了模型检验的一般原理、应用工具及软硬件系统的建模与验证方法，同时介绍了克服模型检验中“状态空间爆炸”问题的有效途径，可作为计算机科学与技术、软件工程等专业本科生、研究生的教材，也可作为模型检验领域研究人员及注重系统可靠性的设计与开发人员的参考书。

赵光峰，男，1964年生，教授，博士，曾留学英国一年，主要研究方向为拓扑学、图论、系统可信性自动验证，发表学术论文30余篇，主编《Visual Basic 程序设计教程》（高等教育出版社）等教材5部。

前 言 公允地说, 在这个数字时代, 正确的信息处理系统比黄金更可贵. ——摘自 H. Barendregt 的“The Quest for Correctness”, 发表于Images of SMC Research 1996，第39~58页. 本书讲述模型检验, 它是一种评估信息及通信系统的功能性质的很好的形式化技术. 模型检验需要考虑系统的一个模型及期望的性质, 并系统地检验给定模型是否满足此性质. 可以验证的典型性质是无死锁、不变性以及请求与响应性质. 模型检验是验证模型不含错误\ (即不违反性质) 的自动技术, 也可看作智能、高效的调试技术. 它是一种通用方法, 已被用于硬件验证及软件工程等领域. 模型检验技术在二十多年前只能用于简单的例子. 但随着基础算法及数据结构的不断改进及硬件水平的进步, 它现在已经可以用于实际设计中. 客观地讲, 过去二十多年中, 模型检验已经发展为成熟的并被大量使用的验证和调试技术. 目的与范围 本书将从基本原理开始介绍模型检验. 本书可作为本科生和研究生的教材, 也可作为计算机科学及相关领域研究者的入门读物. 本书用大量的例子向读者介绍相关的材料, 许多例子会贯穿多个章节. 本书提供完整的基本结论及其详细证明. 每章后面都有总结、文献说明及关于一系列理论与实践(即实际模型检验器的实验) 的习题. 基础知识 模型检验中的概念起源于数学, 例如命题逻辑、自动机理论与形式语言、 数据结构以及图论算法. 尽管本书附录概括了这些内容的要点, 但是读者还是要在学习本书正文前熟悉这些基本知识. 当考虑许多模型检验算法的...