用TLA+定义系统：TLA+语言与工具在软硬件设计中的应用
定 价：139 元
- 作者：[美] 莱斯利·兰伯特（Leslie Lamport） 著，董路明，贺志平 译
- 出版时间：2021/4/1
- ISBN：9787111678229
- 出 版 社：机械工业出版社
- 中图法分类：TP311.11
- 页码：328
- 纸张：胶版纸
- 版次：1
- 开本：16开
本书是作者针对分布式并发计算系统超过25年的研究成果的总结。在本书中，作者提出用基于动作的时态逻辑（TLA）来为复杂信息系统的行为建立数学模型，进而使用严格的数学证明与检验的方法来验证系统行为的正确性。为此，作者发明了建模语言TLA+以及模型检查工具TLC。本书结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。
本书将指导你如何使用TLA+语言编写计算机系统规约。全书篇幅比较长，但大多数人只需要阅读第一部分的内容就够了，这部分包含了大多数工程师需要了解的与编写规约有关的知识，至于学习它所需要的背景知识，只要求具备工程学或计算机科学的本科生所应掌握的数学和计算机知识即可。第二部分将为需要进阶的读者提供更深入的内容。本书的其余部分是参考手册——第三部分介绍TLA+工具，第四部分介绍TLA+语言本身。 TLA官网http://lamport.org有可供下载的配套资源，包括TLA+工具、练习、参考资料和勘误清单。你也可以在搜索引擎上输入uidlamporttlahomepage来找到上述页面，但请不要把这个字符串放到互联网上共享。 何为规约 写作是发现你的想法有多么草率的根本方法。 ——Guindon 规约是“系统应该做什么”的书面定义。定义一个系统有助于我们更好地理解它。在构建系统之前最好先理解该系统，因此在实现之前先编写系统规约是个好主意。 本书讲述了系统的行为属性，也可称之为功能属性或逻辑属性。这些属性定义系统应该做什么。当然系统还有其他我们这里不考虑的重要属性，比如性能属性。最差情况下的性能通常可以表示为行为属性，在第9章我们讲述了如何定义系统在一定时间内的行为，不过，本书暂时不考虑如何定义平均性能。 我们编写规约的基本工具是数学。数学是一门严谨的语言，比自然语言（例如英语或中文）更为精准。在工程实践中，不精准就很容易出错，因此科学和工程学通常采用数学作为基本语言。 本书用到的数学语言会比你一直使用的数学语言更形式化一些。相对于形式化数学，大多数数学家和科学家在写作中使用的数学表达方式并不十分精准，应用于小范围还勉强可以，应用于大范围则不佳。在非形式化数学语言中，每个方程都是一个精确的断言，但你必须阅读方程前后的解释性文字才能理解方程之间的关系以及定理的确切含义。逻辑学家已经研究出了消除这些解释性文字并使数学更形式化、更精准完备的方法。 大多数数学家和科学家可能认为形式化数学又长又乏味，这是不对的，普通数学也可以用一种精准完备的形式化语言来简洁表达。例如在第11章关于微分方程的Diffeential-Equations模块中，只需要用20多行就可以定义任意微分方程的解。不过很少有规约需要用到如此深奥的数学知识，大多数时候只需要简单应用一些基础数学概念即可。 为何是TLA+ 我们通过描述在执行过程中可能会发生的行为来定义系统。1977年，AmirPnueli引入了时态逻辑（temporallogic）来描述系统行为。从理论上讲，系统可以用单个时态逻辑公式表示，但在实际运用上却有些问题：它虽然能很理想地描述系统的某些属性，但在描述其他属性上却不太方便。因此，我们通常将它与更传统的系统表示方式结合在一起来定义系统。 也可称为时序逻辑或时间逻辑，在本书中为了术语统一，均译为时态逻辑。——译者注 在20世纪80年代后期，我发明了TLA，即基于动作（Action）的时态逻辑——这是Pnueli初始逻辑的简单变体。TLA使得用单个公式表示系统变得切实可行。TLA规约的大部分由普通的、非时态逻辑的数学公式组成，时态逻辑仅在其擅长描述的属性中引入并发挥作用。TLA还给出了一种很友好的系统推理模式，这种模式被称为断言式推理（assertionalreasoning），其在实践中被证明是最有效的。不过，本书仅涉及规约本身，较少引入数学证明。 TLA+版本2对证明做了大量改进，参见19.7节。——译者注 时态逻辑使用了一套基本逻辑来表示普通数学，还有许多其他方法也可以使普通数学形式化。大多数计算机科学家都喜欢使用与他们熟悉的编程语言近似的语言，相反，我选择了大多数数学家更喜欢的方法，逻辑学家将其称为一阶逻辑和集合论。 TLA为描述系统提供了数学基础。要编写规约，我们需要在此基础上构建完整的语言体系。我最初认为该语言应该是某种抽象的编程语言，其语义将基于TLA。一开始我不知道用哪种编程语言结构最好，于是决定直接用TLA编写规约，计划在需要时再引入编程语言。令我惊讶的是，到后来我发现不需要了，我所需的就是一种编写数学公式的健壮语言。 尽管数学家已经发展了编写公式的科学，但他们还没有将其转化为工程学科，他们为小规模的数学模型开发了符号语言，但对于大型应用还没有好的方法，因为真实系统的规约可能长达数十页甚至数百页。数学家知道如何编写20行的公式，但对长达20页的公式却束手无策。因此，我不得不在语言中引入书写长公式的符号方法，这些方法的形成得益于我从编程语言中学到的将大型规约模块化的思路。 我将这种语言称为TLA+。在编写不同离散系统的规约时，我不断对TLA+进行提炼和改进，直到后来TLA+趋于稳定。我发现TLA+可以很好地定义从应用程序接口（API）到分布式系统的各种系统。它可以用来为几乎任何类型的离散系统编写精准的形式化定义，尤其适合描述异步系统，即组件运行不严格遵循锁步操作（lock-step）的系统。 关于本书 本书的第一部分包括第1～7章，是本书的核心，需要从头到尾阅读。它描述了如何定义称为安全属性的一类属
书单推荐
