モデル検査

形式システムをアルゴリズム的に形式的検証・検証する手法。ハードウェアソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。