Simulink Design Verifier 使用形式化方法来识别模型中隐藏的设计错误。它检测模型中会导致运行时错误和不良行为的操作，例如整数溢出、死逻辑、数组访问违规和除以零。分析工作分布到各 CPU 内核上以加速获得复杂模型的结果。
Simulink Design Verifier 执行形式化验证，以证明设计满足功能需求且不违反安全需求。形式化分析还验证需求的一致性和完整性。对于每个设计错误或需求违规项，软件会生成一个仿真测试用例以供调试。
使用 Simulink Design Verifier，您可以自动生成测试向量以实现模型和代码覆盖率。这些测试向量驱动您的模型，以实现决策、条件和修正条件/决策 (MC/DC) 覆盖率度量。
通过 IEC Certification Kit（适用于 IEC 61508 和 ISO 26262）和 DO Qualification Kit（适用于 DO-178 和 DO-254），可提供对行业标准的支持。
检测运行时和诊断错误
在运行仿真之前，您可以检测潜在运行时错误和建模问题，包括整数溢出、除以零和数组越界错误；次正规值和其他浮点错误；以及数据有效性错误。使用缺陷检查器进行快速、有针对性的交互式错误检查。
分析测试覆盖率缺失
自动生成测试向量，以增强和扩展现有手动创建的测试用例。使用扩展后的测试用例，弥补模型覆盖率以及从 Simulink 模块和 Stateflow 图中调用的 C/C++ 代码覆盖率的不足。
验证形式化安全需求
验证您的设计是否符合使用 MATLAB、Simulink 和 Stateflow 表达的形式化定义的安全需求。
产品资源：
“基于模型的设计支持快速分析需求，重用以前产品的设计，并消除手动编码错误，从而减少了开发时间，使我们能够缩短工期以满足客户的需要。”
Simulink Design Verifier 常见问题解答
Simulink Design Verifier 使用形式化方法识别模型中隐藏的设计错误，验证设计满足功能需求，并为模型覆盖率和自定义目标生成测试用例。
它检测会导致整数溢出、死逻辑、数组访问违规、除以零、次正规值、浮点错误和数据有效性错误的模型元素。
死逻辑指您的模型中在仿真或执行所生成代码期间无法激活的逻辑。由于此逻辑永远无法执行，因此无法被测试，并且可能表明存在设计或实现错误。Simulink Design Verifier 使用形式化分析来识别这种无法激活的逻辑，并帮助您在开发过程的早期检测潜在问题。
它会自动生成测试用例，以满足条件、决策、修正条件/决策 (MCDC) 和自定义覆盖率目标。它还可以从系统需求模型生成基于需求的测试用例。
它可以验证您的设计是否按照使用 MATLAB、Simulink 和 Stateflow 形式化定义的安全需求运行，并且它为每个设计错误或需求违规生成仿真测试用例以进行调试。
是的，配合 IEC Certification Kit（适用于 ISO 26262 和 IEC 61508）和 DO Qualification Kit（适用于 DO-178 和 DO-254），可实现对行业标准的支持。
它分析缺失测试覆盖率，并增强现有手动创建的测试用例，以弥补模型覆盖率以及从 Simulink 模块和 Stateflow 图中调用的生成 C/C++ 代码覆盖率的不足。
它可以在您开始实现设计之前，使用 Requirements Table 模块检查建模需求的一致性和完整性。
