Model Checking。形式検証法の検証方法の1つで、システム仕様を表現したモデルが、システムに要求されるプロパティ（性質）を満たすか否かを自動的に検査し、システムの正しさやバグを発見する方法です。この手法は、ハードウェアの論理回路や通信プロトコールの正しの検証に用いられ、近年では、ソフトウェア仕様の検証に適用されてきています。モデル検査法は、一般的に、二分決定グラフ（BDD）法と充足可能性判定手法（SAT手法）に大別することができます。Ansys SCADEのモデル検査手法は、後者の充足可能性判定法（SAT法）を用いてプロパティ検証を行います。