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 两类。