模型检验（Model Checking）

🔍 “自动检查系统有没有 Bug”——但不是测试

软件测试：跑几个用例，看看对不对——但”几个用例”只能覆盖一小部分路径。

模型检验：穷举搜索系统所有可能的状态——自动检查是否违反规范。

🏪 **类比：自动扫地机的巡逻路线”

测试 = 你让扫地机走几圈——没撞到东西——“看起来没问题”。

模型检验 = 你建了一个扫地机的数学模型，交给计算机——计算机枚举所有可能的路线——确保没有一条路线会撞到东西。

如果你家有 1000 个角落——每跑一圈只能试一个——但模型检验一次就把所有角落都检查了。

---

🔧 模型检验三步

第 1 步：建模（Modeling）
把系统抽象成状态机：
  - 状态（State）：系统在某一时刻的全部变量值
  - 转移（Transition）：从一个状态到另一个状态的变化

第 2 步：规范（Specification）
用逻辑语言描述"系统必须遵守的性质"：
  - "永远不能死锁"
  - "请求最终会被响应"

第 3 步：验证（Verification）
工具自动搜索所有状态——检查是否违反规范

时序逻辑（Temporal Logic） —描述”随时间变化”的性质：

LTL（线性时序逻辑）：
G p      → Globally p —— p 永远成立
F p      → Finally p —— p 最终会成立
X p      → Next p ——下一步 p 成立
p U q    → p Until q —— p 成立直到 q 成立

例子：
G ¬deadlock            → "永远不死锁"
G (request → F grant)  → "每次请求最终都会被批准"

---

🏢 实际应用

工具	特点	著名用户/应用
TLA+	系统设计规范语言	Amazon（AWS 的 DynamoDB、S3）
NuSMV	符号模型检验	学术界广泛使用
SPIN	分布式协议验证	NASA（验证火星任务软件）
CBMC	C 程序模型检验	嵌入式系统验证

Amazon 如何使用 TLA+：

Amazon 在开发 DynamoDB、S3 等核心服务时——先写 TLA+ 规范
→ 模型检验发现分布式协议中的 bug
→ 在上线前修复——避免生产环境事故

效果：TLA+ 发现了一些测试发现不了的设计缺陷

---

⚖️ 模型检验的局限

长处：自动、穷举、产生反例
局限：状态爆炸——系统状态数随变量数量指数增长

缓解方式：
- 符号模型检验（BDD）
- 抽象（Abstract Interpretation）
- 有界模型检验（限制搜索深度）

---

📝 小结

概念	一句话
模型检验	穷举搜索所有状态——自动验证系统正确性
时序逻辑	LTL/CTL——描述”随时间变化”的规范
状态爆炸	状态数随变量数量指数增长——主要挑战
TLA+/NuSMV/SPIN	主流的模型检验工具
反例	模型检验违反规范时——提供一个具体的违规路径

为什么先学这个？ 模型检验是”自动验证”。另一种更强大的验证方式——定理证明（Coq, Lean）——需要人工指导但能验证任意性质。