Main Content

本页采用了机器翻译。点击此处可查看英文原文。

带模块替换的定点巡航控制的属性证明工作流程

打开脚本

此示例说明如何证明定点巡航控制算法中的属性。它通过模型引用来引用设计模型，使得原有的设计模型保持不变。模块替换规则指定检查是否可能发生溢出的属性。验证子系统指定了属性证明时对速度输入范围的假设。该模型配置 Simulink Design Verifier 以将模块替换应用于 Sum模块，该模块为引用模型中的定点 PI 控制器的输出端口提供数据，并返回演示溢出的反例。

open_system('sldvdemo_cruise_control_fxp_verification');