主要内容

用MATLAB函数块证明性质

这个例子展示了如何验证安全带提醒设计模型。它下面的安全属性块包含一个在MATLAB中指定的属性,该属性指示图标何时应该被激活。金宝appSimulink设计验证器通过分析设计模型和安全特性来证明其正确性或识别反例。在这个模型中,违反了这个属性,因为设计隐式地假定KEY输入从0开始,并以1为增量进行更改。

open_system (“sldvdemo_sbr_verification”);