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 つのオブジェクティブが反証されたことがレポートされます。

ハーネス モデルが生成され、[Signal Builder] ダイアログ ボックスが開き、反例が表示されます。

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

[Signal Builder] ダイアログ ボックスで、[シミュレーションの開始] ボタン ▸ をクリックします。

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

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

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

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

open_system('sldvdemo_cruise_control_verification_fixed');

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

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

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

参考