Simulink Design Verifier
识别设计错误、证明需求合规及生成测试
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），可提供对行业标准的支持。
开始:
死逻辑
查找模型中在仿真和执行生成的代码时无法激活的对象。 |
查看模型中的死逻辑。
基于需求的测试用例
从系统需求模型生成测试用例。
用于 C/C++ 代码的测试用例
生成测试用例以增加生成的代码以及从 Simulink® 模块和 Stateflow® 中调用的 C/C++ 代码的覆盖率。
为调用 C 代码的模型生成测试。
安全需求
验证您的设计是否符合使用 MATLAB®、Simulink 和 Stateflow 表达的形式化定义的安全需求。
针对 System object 检测查错误
使用Simulink中的System对象，来为 MATLAB 代码检测错误、生成测试或证明属性
检查是否违反了高完整性系统建模 (HISM) 指南规范
检查是否违反了特定的 HISM 指南规范，例如使用数学函数模块作为平方根模块
启用实现快速死逻辑检查
首先在设计阶段附近的时间点就开始快速运行部分死逻辑检查，后续再投入计算时间来进行穷尽式的分析
（从 R2020a 重用）总线元素支持
分析包含输入或输出总线元素模块的顶层模型
（从 R2020a 重用）改进的死逻辑报告
在“结果检查器”窗口中查看死逻辑的可能原因，包括 short-circuit 逻辑和条件执行
（从 R2020a 重用）并行测试用例验证
使用并行计算验证测试用例或反例
关于这些功能和相应函数的详细信息，请参阅发行说明。
