以前モデルベースドテストについての記事を書いて、

モデルをテスト対象にしたテストをモデルベースドテストだと勘違いするケースが多いので、そこだけは、間違えないようにしてください。

と言いました。今日似たような中に「モデル検査（検証）」が出現しましたので、追加します。

モデル検査はこちらです。

モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。

とのことです。ISO/IEC/IEEE 29119-1では、Model checkingはFormal methodの下位に位置付けられています。なお、Formal methodはV&Vの下位に位置付けられ、並列にTestingとV&V Analysisが来ています。

つまり、モデル検査（検証）はモデルベースドテストとも、モデルを対象にしたテストとも全く別物だということが言えます。

改めて、それぞれを簡潔に表現してみます。

モデルベースドテスト：モデルを基にテストケースを作り出す、テスト設計の手法（またはその手法を使ったテストアプローチ）

モデルを対象にしたテスト：モデルの良さを確かめるために実施する（主に）動的テスト

モデル検査（検証）：モデルの良さを確かめるために実施する数学的な検証

こんな感じですかね。正直なところ、形式検証が静的テストの中に含まれるのか含まれないのか、微妙なところだと思っていて、もし含まれるならばモデル検査もモデルを対象にしたテストの一部なのでは、という主張もありそうです。でも、実際世の中的にこれらの言葉が使われるのは明らかに別の文脈になるので、それぞれ区別して使った方がいいのは間違いないと思います。

おわり。