【注】 本文为2018 Mathworks 年会上机教程学习笔记， 讲师：周玲， 如有侵权，立即删除

本文所有模型均为上机练习模型，百度云链接

Simulink Design Verifier

在Simulink中有多种方法对模型进行测试，传统上来讲，验证涉及到用于根据特定的需求创建对应的一系列测试，同事用户还需要根据这些测试用例，给出其预期的结果。测试的创建需要能够覆盖到功能的同事，还需要兼顾系统的稳健性要求。

本例将借助Simulink Design Verifier对模型进行仿真分析，以检查是否存在潜在的始终无法**的状态或转移，以及除以零这样的设计错误。

Simulink Design Verifier的三大功能：

• Design Error Detection —— 查找死逻辑、除以零、溢出等问题
• Test Generation —— 基于模型和覆盖度来生成测试用例，这部分在Step 5中学习
• Property Proving —— 确定模型的输出和行为是满足预期要求的，这部分在Step 7中学习

对模型做死逻辑检测

使用Simulink Design Verifier对模型进行分析，本节的目标是查找模型中的死逻辑（即无可能被执行到的逻辑），这里仅查找死逻辑，但实际上这种方法还可以用来查找溢出等问题。

Analysis > Design Verfier > Options

在Design Verifier的Design Error Detection中勾选Dead logic和Identify active logic

Analysis> Design Verifier > Detect Design Errors > Model

之后会出现下图，

显示有两个死逻辑，打开模型可以看到死逻辑的位置

问题分析

Simulink给出的问题是after(incdec/holdrate10,tick) 不可能为false，为什么？进入断点调试

运行模型，并在Command Window中做调试

这里我们可以看到问题了，当用整型数据替换掉浮点型数据后，上面的两个转移条件永远都是0，解决方法，将 **after(incdec/holdrate10,tick)** 改为after(10*incdec/holdrate,tick)

模型除以零的检测

打开示例模型，
Analysis, Design Verifier, and Options

在Design Error Detection ** 勾选check Division by zero**，点击OK

Analysis > Design Verifier > Detect Design Errors > Model
查看报告，可以看到，当测试用例为holdrate = 0，incdec = 1的时候，出现了不满足的情况

在结果中点击Create harness model，会生成对应的测试用例，运行Tets Case1后报错

这个原因是因为holdrate的最小值为0，我们在Command Window中将这个参数的最小值设置为1，然后重新在Design Verifier中对Paramters进行设置，先勾选参数Clear后重新Find in Model。


再次进行Analysis > Design Verifier > Detect Design Errors > Model，结果如下

自动设计错误检测

在Model Advisor的By Product中就包含了Simulink Design Verifier栏，下设Design Error Detection，可以用来进行检测死逻辑、除以零等设计问题。

总结

在Simulink Design Verifer中进行设计错误的检查，可以针对设计错误自动生成test harness以测试用例，用于帮助用户快速查找问题的根源。