使用 MATLAB Truth Table 模块进行属性证明

打开脚本

此示例说明如何验证上方顶层模块中引用的安全带提醒装置设计模型。该模型下方的 Safety Properties 模块包含在 MATLAB Truth Table 中指定的一个属性，该属性指示 SeatBeltIcon 输出何时应处于活动状态。Simulink Design Verifier 会分析设计模型和安全属性，以证明正确性或识别反例。在此模型中，该属性的证明基于以下显式假设：KEY 输入从 0 开始并以 1 为增量变化。

open_system('sldvexSBRVerificationTruthTableFixedExample');