本页翻译不是最新的。点击此处可查看最新英文版本。

使用 MATLAB Function 模块进行属性证明

打开脚本

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

open_system('sldvdemo_sbr_verification');