分析控制系统模型对建模为属性的需求的遵守情况，并使用依赖分析来调查属性违反情况。

通过使用Simulink®Design Verifier™属性证明分析万博1manbetx来查找属性违规。您将安全需求建模为属性，然后根据需求验证设计模型。

验证反推器设计模型的安全性能。下面的Properties块包含四个安全属性。万博1manbetxSimulink®Design Verifier™分析设计模型和安全属性，以证明正确性或识别反例。模型引用的使用消除了向设计模型添加验证内容的需要，允许验证内容独立于设计而存在。

使用多个属性执行属性证明分析。该模型被配置用于分析，以试图证明:

证明了一个定点巡航控制算法的性质。它使用模型引用引用设计模型，因此原始设计模型是不变的。块替换规则指定检查是否可能发生溢出的属性。验证子系统在属性证明过程中指定了对速度输入范围的假设。该模型配置Simulink Design V万博1manbetxerifier，以将块替换应用到Sum块，该块提供给引用模型中的定点PI控制器的输出端口，并返回一个演示溢出的反例。

使用观察者引用块执行属性证明分析。