手順1:モデルを開く

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

open_system (“sldvdemo_cruise_control_verification”)；

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

open_system (“sldvdemo_cruise_control_verification /安全属性”)；

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

(设计验证器)タブで,[プロパティ証明)をクリックします。

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

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

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

(信号Builder)ダイアログボックスで,[シミュレーションの開始)ボタン▸をクリックします。

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

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

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

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

open_system (“sldvdemo_cruise_control_verification_fixed”)；

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

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

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

参考