主要内容
MATLAB函数块的性质证明
这个例子展示了如何验证安全带提醒设计模型。它下面的安全属性块包含一个在MATLAB中指定的属性，指示图标何时应该是活动的。金宝appSimulink Design Verifier通过分析设计模型和安全特性来证明其正确性或识别反例。在这个模型中，这个属性被违背了，因为设计隐式地假定KEY输入从0开始，并以1为增量进行更改。
open_system (“sldvdemo_sbr_verification”);
你也可以从以下列表中选择一个网站:
