モデルベーステスト
本来、モデル検査はモデルが仕様を満足するかを検証する技法として開発された。モデルベーステストに応用する場合、テスト対象システムのモデルとテストしたい属性をモデル検査機に与える。モデル検査機はその属性がモデル上で正しいかどうかを証明する過程で証拠と反例を検出する。証拠となる経路はその属性を満足する。一方、反例となる経路を実行すると、その属性に反した状態となる。これらの経路がテストケースとして使用できる。