形式化验证和 TLA+ 入门

这篇文章的目的是让读者了解：

• 为什么存在形式化方法以及为什么这些方法在分布式系统领域特别重要。
• TLA+ 简介，包括它如何表示数据和时间的概念模型。

为什么使用 TLA+ 或任何其他形式验证技术？
设计并发和分布式系统等复杂系统很困难。复杂性源于需要平衡众多相互竞争的需求，例如性能、可扩展性、容错性、安全性和资源成本。设计人员必须维护一个由依赖关系、交互和潜在故障点组成的复杂网络的心理模型。这不是一件容易的事。

形式化建模是系统设计者工具包中的一个强大工具。它提供了一种精确且明确的方式来表示系统的行为和结构，为工程师提供了一种精确的语言来描述复杂的细节和潜在的交互，而这些细节和潜在的交互可能会被非正式的描述和工程师自己对系统的内在理解所忽视。通过模型，您可以更好地了解设计，几乎可以用手拿起。

它和其他任何东西一样，都是一种沟通工具。我喜欢将其视为一个可执行且可验证的图表工具，同时也是一个模拟器，可以帮助我分析系统在各种条件下的行为。

属性和原则
系统设计师非常重视原则和属性，在设计和构建复杂系统时将其作为指导。

原则可以是"系统应尽可能多地采用去中心化和无状态的组件，以增强弹性 "或 "系统应能够自我修复和恢复，而不是依赖人工干预"。原则无法通过机器验证，但系统设计者可以知道原则是否得到遵守以及遵守的程度。原则就像项目的指路明灯，帮助团队做出更好的架构决策。

属性更为具体，实际上是可以通过机器验证的--可以证明系统是否满足某个属性。属性可能包括以下内容"只要一台服务器还在运行，系统就应该保持可用 "或 "客户端必须能够读取自己写入的内容 "或 "分布式死锁最终会被检测到"。系统设计者非常关心这些属性，并首先定义关键属性，这样他们就能设计出满足这些属性的系统。

使用形式化方法，我们可以将问题分解为系统的形式化模型和系统应遵循的属性。通过识别违反这些属性的行为来发现缺陷。

主要有两种方法：

• 构建数学证明。
• 使用模型检查器对所有可能的相互作用进行强行搜索，并标记出任何会导致违反属性的相互作用。这就是所谓的有界模型检查。

构建证明是一项艰苦的工作，比使用有界模型检查要花费更多的精力。我个人使用模型检查，因为它简单实用，足以让我在繁忙的其他工作中兼顾规范编写。

TLA+ 简要指南
当我们在 TLA+ 中为一个系统建模时，我们是在为它的设计建模，而不是在为它的实现建模。我们模拟的是它应该做什么，而不是它应该如何做。建模的部分目的是为了更多地了解所提议的系统，并与他人分享设计，因此清晰和简洁非常重要。我们不会对系统的每一个细节都进行建模，而是选择一个合适的抽象层次。系统的许多方面都可以被视为优化或实现细节，可以不列入我们的规范中。

在 TLA+ 规范中，"系统应该做什么 "由变量、常量和操作来表示。

• 常量描述了系统中不会改变的方面。这可以是系统中的参与者，也可以是一些阈值
• 变量描述系统的可变状态，如数据或不同参与者的当前状态（服务器是启动还是关闭）
• 操作会修改系统（改变变量），例如发送或接收信息、写入或删除数据。

状态、步骤和时间
在 TLA+ 中，状态是值到变量的映射。

一个 24 小时时钟可以用小时、分钟和秒变量来模拟。一个状态 s1 可以是值到变量的映射：小时=10，分钟=23，秒=38，而状态 s2 可以是：小时=10，分钟=23，秒=39。时钟走一格，系统就从状态 s1 进入状态 s2。

这种时钟规格将有 86400 种可能的唯一状态，因为这是一天中的秒数。

步进是从一个状态过渡到另一个状态。如果时钟跳动 1 秒，那么我们将从 s1 过渡到 s2，其中 s2 比 s1 提前 1 秒。

时间不是连续的，而是以离散的单位--状态--来表示的，每一步都是从一个状态过渡到另一个状态。

s1 -> s2 -> s3 -> s4 ... sN
我们描述的是系统的初始状态，甚至是系统开始时的多种可能状态。描述 "系统应该做什么 "的操作将使系统过渡到后续状态。

特性：安全性和有效性
我们将属性分为两类：安全性和有效性。

安全属性的重点是坏事不会发生。使用最广泛的安全属性类型是不变量。不变量是指在每个可达到的状态下都必须始终为真的属性--一旦它为假，就意味着我们违反了安全性。数据丢失就是一个例子。不变量可以声明，放入袋中的每件物品都必须永远在袋中找到。但是，如果袋子上有一个洞，物品可能会掉出来，这将立即违反该不变式。

不变式只涵盖单个状态，但我们也可能需要一个描述状态间非法转换的安全属性。例如

塑料袋绝不能从 "满 "状态变为 "回收 "状态，它必须首先处于 "空 "状态。

状态 s+1 的时钟必须比状态 s 超前一秒。

模型检查
TLA+ 配备了名为 TLC 的有界模型检查器和名为 TLAPS 的证明助手。在我的职业生涯中，我一直专注于模型检查，因为它能为我提供最好的投资回报率；我不能把所有时间都花在建模上，我实际上还需要去构建东西。

模型检查的缺点在于，它所能实现的功能有限。TLC 对所有可能的可达到状态进行粗暴的广度优先搜索（BFS）。有些规范的状态空间可能非常大，甚至是无限大，这就使得蛮力模型检查变得不可行。限制状态空间的大小往往是必要的。

有效性属性描述的是最终必须发生的好事。例如，如果鲍勃给爱丽丝寄明信片，爱丽丝最终一定会收到。或者，如果我不断往袋子里放东西，袋子最终一定会装满。然而，如果邮递员清空邮筒时明信片掉了，那么就违反了有效性属性，因为爱丽丝永远也收不到明信片。如果袋子上有个洞，那么物品可能会以与添加速度相同的速度掉出来，导致袋子永远也装不满--这就违反了该属性。

案例点击标题