Main Content

Observer Reference ブロックを使用したプロパティ証明解析

この例では、Observer Reference ブロックを使用し、モデルに変更を加えることなく、複数のプロパティによるプロパティ証明解析を実行する方法を説明します。この例では、既存の検証サブシステムを Observer Reference ブロックに置き換えます。ただし、モデルに置き換える検証サブシステムがない場合でも、モデルに Observer Reference ブロックを追加できます。詳細については、Access Model Data Wirelessly by Using Observers (Simulink Test)を参照してください。

モデル sldvdemo_debounce_validprop は解析用に構成されており、以下の証明を試行します。

  1. 現在の入力値および以前の 6 つの入力値が true の場合、出力は true になる。

  2. 現在の入力値および以前の 6 つの入力値が false の場合、出力は false になる。

Observer Reference ブロックの詳細な説明については、オブザーバーによる検証ロジックの分離を参照してください。

手順 1: モデルを開く

モデル sldvdemo_debounce_validprop には、Verify Output という検証サブシステムが含まれています。検証サブシステムの詳細については、Verification Subsystemを参照してください。モデルを開くには、次を入力します。

open_system('sldvdemo_debounce_validprop');

手順 2: 検証サブシステムを Observer Reference ブロックに置換

次の手順を実行し、新しい Observer Reference ブロックを作成して Verify Output 検証サブシステムと置き換えます。

1.Verify Output サブシステムを右クリックします。コンテキスト メニューで、[オブザーバー][選択したブロックをオブザーバーに移動][新規オブザーバー] をクリックします。

2.表示されたダイアログ ボックスで [はい] をクリックします。

3.検証サブシステムが Observer Reference ブロックに置き換えられます。オブザーバー モデル sldvdemo_debounce_validprop_Observer1 が開きます。

4.sldvdemo_debounce_validprop_Observer1 を MATLAB パス上の書き込み可能なフォルダーに保存します。

5.Observer Port ブロックをダブルクリックして [Observer ブロックの管理] ウィンドウを開きます。2 つの信号 debounce と raw がオブザーバー モデル sldvdemo_debounce_validprop_Observer1 内の 2 つの Observer Port ブロックに自動的にマッピングされます。

手順 3: プロパティ証明解析の実行

プロパティ証明解析を実行するには、次の手順に従います。

1.最上位モデルの [Design Verifier] タブで、[プロパティ証明] をクリックします。

2.解析が終了した後、[Simulink Design Verifier の検証結果の概要] ウィンドウで、2 つのオブジェクティブが達成されたことが報告されます。

3.HTML 解析レポートを開き、最上位モデルとオブザーバーに関する情報を含む詳細レポートを確認します。

手順 4: プロパティ証明解析レポートの確認

解析レポートでは、プロパティの章のオブザーバー モデルの節にプロパティ証明用のオブザーバー情報が示されています。

モデルを閉じます。

bdclose('all');

関連するトピック