Simulink Design Verifier 快速入门

识别设计错误，证明需求符合要求并生成测试

Simulink^® Design Verifier™ 使用形式化方法来识别模型中隐藏的设计错误。它可以检测模型中导致整数溢出、死逻辑、数组访问违规和除以零的模块。它可以通过形式化方式验证设计是否满足功能需求。对于每个设计错误或需求违规，它都会生成一个用于调试的仿真测试用例。

Simulink Design Verifier 可为模型覆盖率和自定义目标生成测试用例，以扩展基于需求的现有测试用例。这些测试用例可驱动您的模型满足条件、决策、修正条件/决策 (MCDC) 和自定义覆盖率目标。除覆盖率目标之外，您还可以指定自定义测试目标以自动生成基于需求的测试用例。

对行业标准的支持可通过 IEC Certification Kit (for IEC 61508 and ISO 26262) 和 DO Qualification Kit (for DO-178) 获得。

致谢

教程

关于使用 Simulink Design Verifier 进行系统模型验证

Simulink Design Verifier 的特征和功能概述，帮助您开始进行形式化验证。
Simulink Design Verifier 工作流程概述

基本Simulink Design Verifier工作流程概述。
检测控制器模型中的设计错误

使用设计错误检测分析来识别模型中隐藏的设计错误。
为简化巡航控制模型生成测试用例

分析演示 Simulink Design Verifier 功能的简单控制系统模型。

精选示例

检测整数溢出错误

此示例展示如何使用设计错误检测分析来检测模型中的整数溢出错误。Simulink® Design Verifier™ 识别可能导致整数溢出的模型构造，然后证明整数溢出在仿真期间不会发生，或者生成演示整数溢出错误的测试用例。

打开脚本

Cruise Control 的财产证明工作流程

此示例显示如何使用 Simulink® Design Verifier™属性证明分析来查找属性违规。您将安全需求模型为属性，然后根据需求验证设计模型。

打开脚本

此示例说明如何生成实现完整模型覆盖率的测试用例。默认情况下，Simulink® Design Verifier™ 会以最少的步骤生成满足目标的测试用例。测试目标之一是强制 PI 控制器中的离散积分器超过其上限。当您无限制约束运行Simulink Design Verifier时，通过强制速度为 500，只需一步即可超出限制。速度约束将测试用例的值限制在 0 到 100 之间。这会强制测试用例采取多个样本以超出积分器的限制。