Reading Papers - Model Checking Overview
# 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 。
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 ;
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01