Simulink Design Verifier 使用形式化方法来识别模型中隐藏的设计错误。它检测模型中导致整数溢出、死逻辑、数组访问越界和除以零的块。它可以形式化验证设计是否符合功能需求。对于每个设计错误或需求违规项，它会生成一个仿真测试用例以供调试。
Simulink Design Verifier 可以生成测试用例以满足模型覆盖率和自定义目标，从而扩展现有的基于需求的测试用例。这些测试用例有助于您的模型满足条件覆盖率、决策覆盖率、修正条件/决策覆盖率 (MCDC) 以及自定义覆盖率目标。除了满足覆盖率目标外，您还可以指定自定义的测试目标来自动生成基于需求的测试用例。
配合 IEC Certification Kit (for ISO 26262 and IEC 61508) 和 DO Qualification Kit (for DO-178 and DO-254)，可实现对行业标准的支持。
检测运行时和诊断错误
在运行仿真之前，您可以检测运行时和建模错误，包括整数溢出、除以零、数组越界、非规范值、浮点误差以及数据有效性错误。
分析测试覆盖率缺失
增强和扩展现有手动创建的测试用例，以解决不完整的模型覆盖率以及从 Simulink 模块和 Stateflow 图中调用的生成代码和 C/C++ 代码的覆盖率。
验证形式安全需求
验证您的设计是否符合使用 MATLAB、Simulink 和 Stateflow 表达的 形式化定义的安全需求 (3:53)。
产品资源:
“基于模型的设计支持快速分析需求，重用以前产品的设计，并消除手动编码错误，从而减少了开发时间，使我们能够缩短工期以满足客户的需要。”
