Reading Papers - Model Checking Overview

# Model Checking Taxonomy

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

in-situ 指的是“就地”运行被测系统，使测试与通常执行时的运行情况尽可能接近，并且通常会尽可能减少对被测系统的侵入性修改。这是对现代复杂软件系统进行 model checking 的主要策略。
abstraction-based 指的是为被测系统进行一定程度的抽象，基于抽象模型进行 model checking 。这是我口胡的，大概等我重新 survey 一下 model checking 的 paper 会有一个更准确的 taxonomy 。
formalized 指的是对被测系统进行完全的抽象，以形式化语义描述和验证被测系统的某些属性。这是过去形式化社区所用的 model checking 策略。

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