この例では、シート ベルト リマインダーの設計モデルを検証する方法を示します。その下の Safety Properties ブロックには、アイコンをアクティブにすべきタイミングを示す MATLAB で指定されたプロパティが含まれます。Simulink Design Verifier は正確性を証明または反例を同定するために、設計モデルおよび安全性プロパティを解析します。このモデルでは、設計でキー入力が 0 で開始されて 1 のインクリメントで変更されると仮定されるため、プロパティ違反が発生します。

この例では、一番上のブロックで参照されるシート ベルト リマインダーの設計モデルを検証する方法を示します。その下の Safety Properties ブロックには、SeatBeltIcon 出力をアクティブにすべきタイミングを示す MATLAB Truth Table で指定されたプロパティが含まれています。Simulink Design Verifier は正確性を証明または反例を同定するために、設計モデルおよび安全性プロパティを解析します。このモデルでは、キー入力が 0 で開始されて 1 のインクリメントで変更されるという明示的な仮定に基づいてプロパティは証明されます。

この例では、Proof Assumption ブロックを使用した、Simulink Design Verifier のプロパティ証明の実行方法を示します。これは、現在の入力値および以前の 6 つの入力値の合計が 6 より大きい場合、出力が 2 と等しいことを証明しようとします。モデルには入力を 0 または 1 に制約する Proof Assumption ブロックが含まれます。Simulink Design Verifier は 20 以下のタイム ステップの違反を検索します。仮定に基づいてプロパティが有効であるため、違反を見つけることはできません。

この例では、Simulink Design Verifier のプロパティ証明解析を使用した、無効なプロパティの検索方法を示します。これは、現在の入力値および以前の 6 つの入力値の合計が 6 より大きい場合、出力が 2 と等しいことを証明しようとします。この場合、単一の大きな入力値 (255 など) によって合計が 6 より大きくなるため、プロパティは無効です。Simulink Design Verifier はこの違反を示す反例を生成します。