金宝app^®Design Verifier™は形式的手法を使用することで,大規模なシミュレーションを実行せずにモデル内の隠れた設計エラーを特定します。整数のオーバーフロー、デッド ロジック、配列アクセスにおける違反、ゼロ除算および要件違反を引き起こすブロックをモデル内で検出します。各エラーについてデバック用のシミュレーション テスト ケースが生成されます。

Simulink Design Verifierはモデル カバレッジとカスタムのオブジェクティブ用のテスト入力を生成します。また、既存テスト ケースの増強および拡張を行うこともできます。これらのテスト ケースによりモデルは条件、判定、改良条件判定 (MCDC) およびカスタムのカバレッジ オブジェクティブを達成できます。

Simulink Design Verifierのモデル スライサー ツールは動的解析と静的解析を組み合わせて使用することで、モデルの問題がある動作を分離します。これを使用して端子、信号およびブロックの機能の依存関係を強調表示およびトレースできます。また、解析用に大規模モデルをより小規模なスタンドアロンのモデルにスライスできます。サブシステムの出力に影響しているブロックを確認したり、複数のスイッチおよびロジックを通る信号パスをトレースできます。バリアント リデューサー ツールでは、アクティブなバリアント コンフィギュレーションに基づいてスライス モデルを作成することにより、複数のバリアントを含むモデルを簡略化できます。

業界標準には、IEC Certification Kit(IEC 61508 と ISO 26262 用) とDO Qualification Kit(DO-178 用) によって対応しています。