前 言

公允地说, 在这个数字时代, 正确的信息处理系统比黄金更可贵.

——摘自 H. Barendregt 的“The Quest for Correctness”,

发表于Images of SMC Research 1996，第39~58页.

本书讲述模型检验, 它是一种评估信息及通信系统的功能性质的很好的形式化技术. 模型检验需要考虑系统的一个模型及期望的性质, 并系统地检验给定模型是否满足此性质. 可以验证的典型性质是无死锁、不变性以及请求与响应性质. 模型检验是验证模型不含错误\ (即不违反性质) 的自动技术, 也可看作智能、高效的调试技术. 它是一种通用方法, 已被用于硬件验证及软件工程等领域. 模型检验技术在二十多年前只能用于简单的例子. 但随着基础算法及数据结构的不断改进及硬件水平的进步, 它现在已经可以用于实际设计中. 客观地讲, 过去二十多年中, 模型检验已经发展为成熟的并被大量使用的验证和调试技术.

目的与范围

本书将从基本原理开始介绍模型检验. 本书可作为本科生和研究生的教材, 也可作为计算机科学及相关领域研究者的入门读物. 本书用大量的例子向读者介绍相关的材料, 许多例子会贯穿多个章节. 本书提供完整的基本结论及其详细证明. 每章后面都有总结、文献说明及关于一系列理论与实践(即实际模型检验器的实验) 的习题.

基础知识

模型检验中的概念起源于数学, 例如命题逻辑、自动机理论与形式语言、 数据结构以及图论算法. 尽管本书附录概括了这些内容的要点, 但是读者还是要在学习本书正文前熟悉这些基本知识. 当考虑许多模型检验算法的理论复杂度时, 还需要 复杂度理论的相关知识.

内容

本书分为10章. 第1章概述模型检验及其特征. 第2章给出作为软件和硬件系统模型的迁移系统. 第3章介绍线性时间性质的安全性质与活性性质的分类, 并阐述公平性的概念. 检验(正则) 安全性质和?正则性质的基于自动机的算法在第4章中论述. 第5章阐述线性时序逻辑 (LTL), 并指出第4章的算法如何用于LTL 模型检验. 第6章论述分支时序逻辑——计算树逻辑(CTL), 并将其与LTL进行比较, 然后指出如何明确地或符号化地进行CTL 模型检验. 第7章论述基于迹、互模拟及模拟关系的抽象. 第8章讲述LTL 和CTL 的偏序约简. 第9章着重介绍实时时间性质与时控自动机. 最后, 本书以概率模型的验证结束. 附录概括了命题逻辑、图论、形式语言以及复杂度理论的基础知识.

如何使用此书

第1章至第6章可作为一学期(每周两次课) 的模型检验入门课程的内容. 在后续一学期的课程中, 可在稍微复习LTL 和CTL 模型检验后学完第7章至第10章的内容.

致谢

本书的写作与扩充花费了5年的时间. 以下同仁通过使用本书的早期版本给予我们支持: Luca Aceto (丹麦奥尔堡大学, 冰岛雷克雅未克大学), Henrik Reif Andersen (丹麦哥本哈根大学), Dragan Boshnacki (荷兰艾因霍温大学), Franck van Breughel (加拿大渥太华大学), Josée Desharnais (加拿大魁北克大学), Susanna Donatelli (意大利都灵大学), Stefania Gnesi (意大利比萨大学), Michael R. Hansen (丹麦技术大学), Holger Hermanns (德国萨尔布吕肯大学), Yakov Kesselman (美国芝加哥大学), Martin Lange (丹麦奥尔胡斯大学), Kim G. Larsen (丹麦奥尔堡大学), Mieke Massink (意大利比萨大学), Mogens Nielsen (丹麦奥尔胡斯大学), Albert Nymeyer (澳大利亚悉尼大学), Andreas Podelski (德国弗莱堡大学), Theo C. Ruys (荷兰特文特大学), Thomas Schwentick (德国多特蒙德大学), Wolfgang Thomas (德国亚琛大学), Julie Vachon (加拿大蒙特利尔大学), 以及Glynn Winskel (英国剑桥大学). 他们中的许多人都给了非常有益的反馈, 使我们得以完善本书.

Henrik Bohnenkamp、Tobias Blechmann、Frank Ciesinski、Marcus Gr?sser、Tingting Han、 Joachim Klein、Sascha Klüppelholz、Miriam Nasfi、Martin Neuh?usser 和Ivan S. Zapreev 给我们提供了许多详细的意见和一些习题. Yen Cao 绘制了部分图形, Ulrich Schmidt-G?rtz 提供了参考文献方面的帮助. 在此 诚挚地感谢他们.

许多人对本书提出过改进建议, 指出过疏漏. 感谢提出宝贵意见的每一位同仁.

最后, 感谢我们在亚琛、波恩、德累斯顿与恩斯赫德的所有学生的反馈和意见.

Christel Baier

Joost-Pieter Katoen