Main Content

このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。

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

この例では、モデル スライサーを使用してプロパティ証明違反をデバッグする方法を説明します。モデル 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_Out0 より大きいため、プロパティは反証されます。

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

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