大家好，我叫Andrew，我是MathWorks的Simulink Design Verifier产品的万博1manbetx开发人员。
在本视频中，我将向您展示如何通过按下按钮来检测设计错误。
万博1manbetxSimulink是一种基于模型的设计工具，设计验证器有助于在开发过程的早期检测Simulink模型中的设计错误，从而节省时间和金钱。
Design Verifier使用形式化方法，这允许它证明某些设计错误永远不会发生，当它们可能发生时，它提供一个测试用例来暴露问题并帮助调试。
首先，我们将打开Simulink工具条上的设计验证器窗格并运行设计验证器。万博1manbetx对于这个分析，Design Verifier将检测模型中的死逻辑。死逻辑是模型永远不能执行的逻辑。
Design Verifier在这个模型中发现了一个死逻辑实例。Design Verifier将用红色突出显示死逻辑的实例，这使查找变得容易。结果检查器窗口准确地告诉我们哪些条件永远不能执行。
这里，tspeed < mintspeed从不为真。原因是这个转换首先捕获tspeed小于mintspeed，然后将mintspeed分配给tspeed。这意味着我们永远不会因为tspeed小于mintspeed而离开这个状态。
实际上，当tspeed等于mintspeed时，我们也希望转换出这种状态，因此我们实际上希望(tspeed小于或等于mintspeed)作为条件。
这是Design Verifier帮助我们改进设计的一个例子。
当我们重新运行分析时，我们现在看到模型被证明没有死逻辑。
接下来，我们将分析模型的运行时错误，即除零错误。与前面一样，我们将按下检测设计错误按钮，design Verifier将自动执行其分析。
在本例中，Design Verifier检测到两个按零除的实例。
Design Verifier的部分强大之处在于，它将为您提供一个可用于帮助调试错误的测试用例。通过按“查看测试用例”，Design Verifier将为您生成一个测试工具，您可以模拟它来调试设计错误。这允许我们使用Simulink的所有调试功能，以便更好地理解问题的原因。万博1manbetx
通过导航到错误，我们可以看到我们正在除以holdrate，在本例中holdrate必须为0。这实际上是我们自己定义的一个值。我们除以它的事实表明，我们不希望这个参数的值为0。在这种情况下，修复错误的方法是更改holdrate参数的规范，以排除0的值，这是我们打算从0开始的—帮助改进我们的设计的Design Verifier的另一个实例!
通过重新运行分析，我们现在看到，该模型已被证明不存在除零误差。
您现在已经了解了如何使用design Verifier自动检测设计错误。以下是design Verifier目前能够检测到的设计错误的完整列表，我们将在未来继续添加更多的错误。
除了设计错误检测之外，design Verifier还能够自动生成测试，并证明模型满足其指定的要求。
非常感谢您的宝贵时间，更多信息请参见视频描述中的链接。
