分析控制系统模型是否符合作为属性建模的需求，并使用依赖关系分析调查属性违反情况。

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

验证反推器设计模型中的安全特性。它下面的Properties块包含四个安全属性。金宝appSimulink Design Verifier通过分析设计模型和安全特性来证明其正确性或识别反例。使用模型引用消除了向设计模型添加验证内容的需要，允许验证内容独立于设计而存在。

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

证明定点巡航控制算法的性质。它使用模型引用来引用设计模型，使原始设计模型保持不变。块替换规则指定检查是否可能溢出的属性。验证子系统在性能证明期间指定了速度输入范围的假设。该模型配置Simulink Design V金宝apperifier以对Sum块应用块替换，Sum块为引用模型中的定点PI控制器的输出提供数据，并返回一个演示溢出的反例。

使用规范模型来执行基于需求的测试。在这个例子中，您遵循一种系统的方法来根据需求验证您的设计模型。有关规格模型的详细描述，请参见什么是规格模型。