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

この例では、Simulink® Design Verifier™ のプロパティ証明解析を使用した、プロパティ違反の検出方法を示します。安全要件をプロパティとしてモデル化してから、要件に対して設計モデルを検証します。

この例では、すべてのモデル カバレッジを達成するテスト ケースの生成方法を示します。既定の設定では、Simulink Design Verifier は最小ステップでオブジェクティブを達成するテスト ケースを生成します。いずれか 1 つのテスト オブジェクティブにより、PI コントローラーの離散積分器がその上限を超過するように強制されます。制約なしで Simulink Design Verifier を実行する場合、速度を 500 に強制することにより、この制限は単一のステップで超過します。速度の制約により、テスト ケースの値は 0 ～ 100 の間で制限されます。これにより、テスト ケースはいくつかのサンプルをとり、積分器の制限を超えるように強制されます。