首页 > 图书中心 >图书详情

模型检验原理

本书是全面、系统地介绍模型检验原理及其应用的鸿篇巨著。

作者:(德)克里斯特尔·拜耳(Christel Baier), (德)乔斯特-皮尔特·卡托恩(Joost-Pieter Katoen)著 赵光峰 李师广 樊丽丽 等译
丛书名:清华计算机图书译丛
定价:158
印次:1-1
ISBN:9787302577355
出版日期:2021.11.01
印刷日期:2021.11.15

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

more >

前 言 公允地说, 在这个数字时代, 正确的信息处理系统比黄金更可贵. ——摘自 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

more >
扫描二维码
下载APP了解更多

同系列产品more >

分布式数据库系统原理(第4版)

(德)塔姆尔·厄兹叙(M
定 价:99元

查看详情
密码学与网络安全(第4版)

(印)阿图尔·卡哈特(A
定 价:79元

查看详情
数字图像的计算几何、拓扑和物理及...

(加)詹姆斯·彼得斯(J
定 价:89元

查看详情
计算机网络(第6版)

(美)安德鲁·S.特南鲍
定 价:138元

查看详情
彩色计算机视觉:基础与应用

(荷)西奥·盖维尔斯(T
定 价:69元

查看详情
图书分类全部图书
more >
  • 赵光峰,男,1964年生,教授,博士,曾留学英国一年,主要研究方向为拓扑学、图论、系统可信性自动验证,发表学术论文30余篇,主编《Visual Basic 程序设计教程》(高等教育出版社)等教材5部。
  • 1.内容全面,条理系统。

    2.实例丰富,便于理解。

    3.理论充实,实践性强

    4.文献翔实,脉络清晰。

    5.习题充足,利于掌握。

    6.附录凝练,入门快速。
more >
  • 目   录

    第1章  系统验证 1

    1.1  模型检验 4

    1.2  模型检验的特征 7

    1.2.1  模型检验的步骤 7

    1.2.2  模型检验的优点与缺点 9

    1.3  文献说明 10

    第2章  并发系统的建模 12

    2.1  迁移系统 12

    2.1.1  执行 15

    2.1.2  硬件和软件系统的建模 16

    2.2  并行与通信 23

    2.2.1  并发与交错 23

    2.2.2  用共享变量通信 26

    2.2.3  握手 32

    2.2.4  通道系统 36

    2.2.5  nanoPromela 42

    2.2.6  同步并行性 51

    2.3  状态空间爆炸问题 53

    2.4  总结 55

    2.5  文献说明 55

    2.6  习题 56

    第3章  线性时间性质 61

    3.1  死锁 61

    3.2  线性时间行为 64

    3.2.1  路径与状态图 64

    3.2.2  迹 66

    3.2.3  线性时间性质 68

    3.2.4  迹等价与线性时间性质 71

    3.3  安全性质与不变式 72

    3.3.1  不变式 73

    3.3.2  安全性质 76

    3.3.3  迹等价与安全性质 79

    3.4  活性性质 82

    3.4.1  活性性质概念 82

    3.4.2  安全性质与活性性质 83

    3.5  公平性 86

    3.5.1  公平性约束 87

    3.5.2  公平性策略 93

    3.5.3  公平性与安全性 94

    3.6  总结 96

    3.7  文献说明 97

    3.8  习题 97

    第4章  正则性质...

精彩书评more >

标题

评论

版权所有(C)2023 清华大学出版社有限公司 京ICP备10035462号 京公网安备11010802042911号

联系我们 | 网站地图 | 法律声明 | 友情链接 | 盗版举报 | 人才招聘