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

この例では次を使用します。

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

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

現在の入力値および以前の 6 つの入力値が true の場合、出力は true になる。
現在の入力値および以前の 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 ブロックに自動的にマッピングされます。