この例では、デバウンサーに対してすべてのモデル カバレッジを達成するテスト ケースの生成方法を示します。このモデル例では、各モデル カバレッジ ポイントの結果がテスト オブジェクティブです。最小のテスト ケースを生成するように Simulink Design Verifier を設定すると、できるだけ多くのオブジェクティブが各テスト ケースで達成されます。

この例では、判定、条件および MCDC カバレッジを達成するテスト ケースの生成方法を示します。Simulink Design Verifier では、テスト データが自動的に生成され、モデルのプロパティが証明されます。テスト基準を満たす入力値のシーケンスが生成されるか、証明の反例が示されます。モデルに関連付けられているコンフィギュレーション オプションで、解析のオブジェクティブを指定します。モデルを解析する場合、Simulink Design Verifier は網羅的探索手法を使用して入力データを生成します。正常に完了するとテスト データが生成され、解析オブジェクティブを満たすデータ値をもつ Signal Builder ブロックを含む新しいハーネス モデルが生成されます。メモ: このモデルの複雑度により、割り当てられた時間内でのテスト生成の完了が妨げられる場合があります。テスト生成を停止して部分的な結果を生成するか、Simulink Design Verifier のオプションを編集して制限時間を延長できます。

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

この例では、フリップフロップに対してすべてのモデル カバレッジを達成するテスト ケースの生成方法を示します。このモデル例では、各モデル カバレッジ ポイントの結果がテスト オブジェクティブです。最小のテスト ケースを生成するように Simulink Design Verifier を設定すると、できるだけ多くのオブジェクティブが各テスト ケースで達成されます。