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

使用Simulink®Design Verifier™属性证明分析发现属性违规。您将安全需求建模为属性，然后根据需求验证设计模型。

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

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

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

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