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

ブロック置換による固定小数点のクルーズ コントロールのプロパティ証明ワークフロー

この例では、固定小数点のクルーズ コントロール アルゴリズムによるプロパティの証明方法を示します。これは、モデル参照を使用して設計モデルを参照するため、元の設計モデルは変更されません。ブロック置換ルールにより、オーバーフローが可能かどうかをチェックするプロパティが指定されます。検証サブシステムにより、プロパティ証明中の速度入力の範囲に対する仮定が指定されます。このモデルは、参照モデルで固定小数点 PI コントローラーの Outport を接続する Sum ブロックにブロック置換を適用し、オーバーフローを示す反例が返されるように Simulink Design Verifier を設定します。

open_system('sldvdemo_cruise_control_fxp_verification');