モデル要件

Simulink^® Design Verifier™ ブロック ライブラリにはサブライブラリ Example Properties が含まれています。Example Properties サブライブラリには以下が含まれます。

• Basic Properties — 基本的なプロパティの証明方法を示す 4 つの例

• Temporal Properties — Boolean 信号の時相プロパティの定義方法を示す 4 つの例

モデルでこれらの例を使用するワークフローは、次のとおりです。

1. これらの例を Verification Subsystem ブロックにコピーします。

2. 証明する個々のプロパティの必要に合わせ、それらを変更します。

3. Simulink Design Verifier 解析を実行して、それらの例のアサーションが決して失敗しないことを証明します。

4. アサーションが失敗すると、アサーションの失敗の原因となる反例が作成され、ハーネス モデルが生成されます。

5. ハーネス モデルで反例を実行して、その反例によりアサーションが失敗することを確認します。

Basic Properties

Basic Properties の例を表示するには、次の手順に従います。

1. Simulink Design Verifier ブロック ライブラリを開きます。次を入力します。

   sldvlib

2. Examples サブライブラリをダブルクリックします。

3. 例が含まれる Basic Properties ブロックをダブルクリックします。

次節以降では、Block Properties サブライブラリ内のそれぞれの例を詳細に説明します。

結果をトリガーする条件

Simulink Design Verifier の Implies ブロックを使用して、結果をトリガーする条件をテストすることができます。この例では、条件 A が true の場合、結果 B は必ず true でなければならないことが指定されています。

信号の増加または減少

この節の 2 つの例では、信号が次のいずれかであることを指定します。

• 常に増加しているか一定

• 常に減少しているか一定

排他的演算

この例では、同時に true にならない 4 つの条件について説明します。

1 つの要素が true の条件

この例では、4 つの入力信号のうち 1 つのみが true に成り得ると指定されています。

Temporal Properties

Temporal Properties の例を表示するには、次の手順に従います。

1. Simulink Design Verifier ブロック ライブラリを開きます。次を入力します。

   sldvlib

2. Temporal Properties サブライブラリをダブルクリックします。

3. 例が含まれる Temporal Properties ブロックをダブルクリックします。

次節以降では、Temporal Properties サブライブラリ内のそれぞれの例を詳細に説明します。

入力と出力の同期

入力 In1 が ACTIVE である場合、5 タイム ステップ後に入力 In2 は INACTIVE に設定されます。

遅延後の信号の非アクティブ化

この例では、SENSOR_HIGH 入力が true となる 5 連続タイム ステップ後に、CMD 信号は true になります。SENSOR_HIGH が true であれば、ブロックが MANUAL_RESET 信号でリセットされない限り、CMD は true になります。

true 信号の拡張

この例では、入力が true になった後、出力は Detector ブロックで指定されたタイム ステップ数だけ true になります (ここでは 5)。入力も 5 タイム ステップの間 true のままです。

指定されたしきい値に対する入力のテスト

入力 In3 が ON であり、入力 In4 が定数 THRESHOLD より小さい場合、In3 は 5 タイム ステップ以内で OFF に設定されます。

関連するトピック

• デバウンス時相プロパティ
• パワー ウィンドウ コントローラー時相プロパティ