このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

モデル スライサーを使用したプロパティ証明違反のデバッグ

この例では、モデル スライサーを使用してプロパティ証明違反をデバッグする方法を説明します。モデル sldvdemo_cruise_control_verification を考えます。このモデルには Assertion ブロックが含まれています。

Verification サブシステムの Safety Properties は、この設計モデルで真でなければならないプロパティをモデル化します。このサブシステムには、プロパティを検証する Assertion ブロック (BrakeAssertion) が含まれています。Simulink Design Verifier のプロパティ検証解析は、アサーションの反証を試みます。それに成功した場合、Simulink Design Verifier は、アサーションを反証する反例を生成します。モデル スライサーを使用して、この反証されたアサーションをデバッグすることができます。

1.モデル sldvdemo_cruise_control_verification を開きます。

open_system ('sldvdemo_cruise_control_verification')

2.[アプリ]、[Design Verifier] をクリックして、Simulink Design Verifier を開きます。

3.[プロパティの証明] をクリックします。Simulink Design Verifier はモデルを解析し、[結果の概要] ウィンドウに結果を表示します。

モデルでは、Assertion ブロックが存在するサブシステムが強調表示されます。

4.Safety Properties サブシステムを開き、反証された Assertion ブロックを選択します。

5.ツールストリップ メニューから [スライサーを使用したデバッグ] をクリックし、モデル スライサーを使用して違反をデバッグします。あるいは、結果インスペクター ウィンドウで [デバッグ] をクリックすることもできます。

いずれかのエントリ ポイントをクリックすると、モデルに対して以下のセットアップが実行されます。

a. Assertion ブロックはモデル スライサーの開始点として追加されます。

b. Simulink Design Verifier の解析によって生成された反例とともにモデルが強調表示されます。

c. 設計モデルがシミュレートされ、アサーション エラーのタイムステップで一時停止します。

6.[ステップを戻す] ボタンと [ステップを進める] ボタンを使用し、端子ラベルを調べて、モデルをデバッグおよび解析します。

• Assert ブロックは、A ならば B (A==>B) の出力が偽であるかどうかをテストします。

• ブレーキ入力 in が 3 つの連続するタイム ステップの間真のとき、A は真になります。

• Throttle_out <= 0 のとき、B は真になります。

条件 A==>B が偽のとき、t=0.04 でシミュレーションが停止することが分かります。このことは、端子ラベルから観察できます。

a. [シミュレーション] タブで、[ステップを戻す] をクリックし、T = (T-0.1) におけるすべてのブロックの端子ラベルを確認します。

A の端子ラベルは、T=0.04 まで偽で、それ以降、真になることが分かります。その時点で、B の端子ラベルは偽 (Throttle_Out > 0) です。Throttle_Out が 0 より大きいため、プロパティは反証されます。

b. 結果が失敗となるブロックを表示するには、[Design Model]、[コントローラー] を開きます。依存ブロックおよびパスが強調表示されます。

修正を表示するには、sldvdemo_cruise_control_verification モデルを開き、キャンバス上の [Open Fixed Model] ボタンをクリックします。