この例では、Simulink® Design Verifier™ でのテスト生成時とプロパティ証明時の両方について、解析の制約として入力端子の最小値と最大値を使用する方法を示します。

この例では、設計エラー検出解析を使用して、モデル内の整数オーバーフロー エラーを検出する方法を示します。Simulink® Design Verifier™ は、結果として整数オーバーフローに至る可能性のあるモデル構造を特定し、シミュレーション中に整数オーバーフローが発生することがないと証明するか、または、整数オーバーフロー エラーを示すテスト ケースを生成するかのいずれかを行います。

モデル内で配列の範囲外へのアクセス エラーを検出

この例は、sldvexCommonCausesOfDeadLogic モデルを使用して、デッド ロジックの原因となっている可能性のある個所を分離する方法を示します。デッド ロジックの検出では、モデル要素が非アクティブで残される原因となる、モデル内の到達不可能なオブジェクティブを見つけます。