Main Content

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

クルーズ コントロール のプロパティ証明ワークフロー

この例では、Simulink® Design Verifier™ のプロパティ証明解析を使用した、プロパティ違反の検出方法を示します。安全要件をプロパティとしてモデル化してから、要件に対して設計モデルを検証します。

プロパティ証明解析を実行すると、Simulink Design Verifier はプロパティ違反をデバッグするために使用する反例を生成します。

手順 1: モデルを開く

sldvdemo_cruise_control_verification モデルには sldvdemo_cruise_control_defective 設計モデルへのモデル参照が含まれます。設計モデルは、実際の速度とターゲット速度間の差に基づいてスロットル出力を計算する PI コントローラーで構成されるクルーズ コントロール システムです。

open_system('sldvdemo_cruise_control_verification');

このスロットル出力の安全プロパティは Assertion ブロックによる Safety Properties 検証サブシステムでモデル化されます。

open_system('sldvdemo_cruise_control_verification/Safety Properties');

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

[Design Verifier] タブで、[プロパティの証明] をクリックします。

解析が完了すると、[結果の概要] ウィンドウに 1 つのオブジェクティブが反証されたことがレポートされます。

ハーネス モデルが生成され、反例が表示されます。

手順 3: エラーを再現する反例のシミュレーション

ハーネス モデルのウィンドウで [すべて実行] ボタンをクリックします。Counterexample_1 ブロックをダブルクリックして [信号エディター] ダイアログ ボックスを開きます。[信号エディターを起動します] ブロック アイコンをクリックして信号エディターを開きます。

[信号エディター] ウィンドウに、時間 0.04 にアサーションが発生したためシミュレーションが終了したことを通知するエラーが表示されます。

オプションで、モデル スライサーを使用してプロパティ違反をデバッグできます。詳細については、モデル スライサーを使用したプロパティ証明違反のデバッグを参照してください。

手順 4: 修正されたモデルを開く

反例で示された誤った動作は sldvdemo_cruise_control_verification_fixed モデルで修正されます。

open_system('sldvdemo_cruise_control_verification_fixed');

プロパティ証明ワークフローで、システムの再設計やプロパティの再定義を行い、その反復処理を実行しなければならない場合があります。

参照モデル sldvdemo_cruise_control_fixed を開き、Controller サブシステムを開きます。このサブシステムでは、アクティブ制御がアクティブな場合に更新された設計モデルによってスロットル出力がリセットされます。

[Design Verifier] タブで、[プロパティの証明] をクリックします。解析が完了すると、[結果の概要] ウィンドウに、オブジェクティブが有効であることがレポートされます。

参考