Main Content

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

使用 MATLAB 函数模块进行属性证明

打开脚本

此示例说明如何验证安全带提醒器设计模型。其下方的安全属性模块包含 MATLAB ® 中指定的属性，用于指示图标何时应处于活动。Simulink ® Design Verifier™ 分析设计模型和安全属性以证明正确性或识别反例。在该模型中，该属性被违反，因为设计隐式假设 KEY 输入从 0 开始并以 1 的增量变化。

open_system('sldvdemo_sbr_verification');