---

Model Checking Taxonomy

Formalized / Abstraction-Based / In-situ

根据测试与通常执行之间的运行情况差别，可以将 model checking 分为三类：

• in-situ 指的是“就地”运行被测系统，使测试与通常执行时的运行情况尽可能接近，并且通常会尽可能减少对被测系统的侵入性修改。这是对现代复杂软件系统进行 model checking 的主要策略。

• abstraction-based 指的是为被测系统进行一定程度的抽象，基于抽象模型进行 model checking 。这是我口胡的，大概等我重新 survey 一下 model checking 的 paper 会有一个更准确的 taxonomy 。

• formalized 指的是对被测系统进行完全的抽象，以形式化语义描述和验证被测系统的某些属性。这是过去形式化社区所用的 model checking 策略。

Stateful / Stateless

根据是否在测试时显式地维护已经探索的状态集合，可以将 model checking 分为 stateful 和 stateless 两类。

---

Uncategorized

EuroSys'23 - Mocket

Mocket 在分布式系统的 TLA+ specification 和 system implementation 之间进行 action-level 的映射，用基于 verified specification 生成的 trace 来运行被测系统，在运行时检查系统状态是否符合 specification 。

• Mocket

• Taxonomy : abstraction-based / stateful model checking / distributed system / TLA+

• Tag : lightweight verification

个人看法：从论文叙述的角度，Mocket 是将 TLA+ specification 上的 verified trace 在粗粒度上映射到实际执行，并在运行时刻进行检查；反过来讲，也可以说 Mocket 是将实际系统行为建模为 TLA+ specification ，验证系统行为是否符合 abstract model 。另一方面，Mocket 仅在粗粒度上控制系统的执行，很大程度上放任真实系统中 non-determinism 的存在，也可以说是一种 lightweight verification 。

Action-Level Mapping

状态和 action ；

---