文档

金宝app设计验证器检查

金宝app设计验证器检查概述

这些检查可以帮助您为模型做准备金宝app®设计验证器™分析。当你运行一个金宝appSimulink设计验证器检查,模型顾问检查金宝appSimulink设计验证器许可证。

有关Model Advisor的更多信息,请参见运行模型顾问检查(金宝app模型)和自动化模型顾问检查执行(金宝app仿真软件检查)。

检查与Simulink设计验证器的兼容性金宝app

检查身份证mathworks.sldv.compatibility

识别Simulink Design Verif金宝appier分析不支持的元素。金宝app

描述

此检查评估您的模型与Simulink设计验证器的兼容性。金宝app

结果和建议的行动

条件 建议的行动
不兼容的

避免在要分析的模型或模型组件中使用以下不受支持的软件功能金宝app或Simulink块:金宝app

部分兼容
兼容的 金宝appSimulink Design Verifier可以分析你的模型。

另请参阅

检测失效逻辑

检查身份证mathworks.sldv.deadlogic

识别在模拟期间保持不活动的逻辑。

描述

此检查确定模型中在模拟期间保持非活动状态的部分。

您可以运行更详细的分析,以识别无效逻辑和活动逻辑金宝appSimulink设计验证器设计错误检测。有关更多信息,请参见检测错误值导致的死逻辑

遵循此检查的建议增加了为嵌入式应用程序生成符合MISRA C:2012标准的代码的可能性,以及符合CERT C和CWE标准的代码

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到的:

也看到处理不兼容的自动存根

在模型中发现死逻辑 金宝appSimulink设计验证器证明了这些决策和条件结果在模型中是不可能发生的,是死逻辑。死逻辑也可能是参数指定约束或输入端口指定最小和最大约束的副作用。在极少数情况下,执行的近似可能导致死逻辑金宝appSimulink设计验证器。有可能存在这种分析没有决定的目标。要扩展此分析的结果,请使用金宝appSimulink设计验证器设计错误检测来识别活动逻辑。在Simulink金宝app编辑器中选择分析>设计验证器>选项。在设计错误检测面板,同时选择死的逻辑识别活动逻辑
在模型中未找到死逻辑 金宝appSimulink设计验证器在模型中没有发现死逻辑。有可能存在这种分析没有决定的目标。要扩展此分析的结果,请使用金宝appSimulink设计验证器设计错误检测来识别活动逻辑。在Simulink金宝app编辑器中选择分析>设计验证器>选项。在设计错误检测面板,同时选择死的逻辑识别活动逻辑

另请参阅

检测超出约束的数组访问

检查身份证mathworks.sldv.arraybounds

检测在数组索引范围之外进行访问的操作

描述

此检查检测Simulink设计验证程序中超出约束的数组访问实例。金宝app

遵循此检查的建议增加了为嵌入式应用程序生成MISRA C:2012兼容代码的可能性,以及符合CERT C, CWE, ISO/IEC TS 17961标准的代码。

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到

也看到处理不兼容的自动存根

在模型中发现超出界限的数组访问

若要查看导致超出边界的阵列访问的条件,请创建线束模型。当您模拟线束时,输入会复制错误。点击查看测试用例在Model Advisor报告中。

另请参阅

检测除零

检查身份证mathworks.sldv.divbyzero

检测模型中的除零错误

描述

此检查识别模型中导致除零错误的操作。

遵循此检查的建议增加了为嵌入式应用程序生成MISRA C:2012兼容代码的可能性,以及符合CERT C, CWE, ISO/IEC TS 17961标准的代码。

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到

也看到处理不兼容的自动存根

除零在模型中找到

要查看导致除零的条件,请创建线束模型。当您模拟线束时,输入会复制错误。点击查看测试用例在Model Advisor报告中。

另请参阅

检测整数溢出

检查身份证mathworks.sldv.integeroverflow

检测模型中的整数或定点数据溢出错误

描述

此检查标识超出整数或定点操作的数据类型范围的操作。

遵循此检查的建议增加了为嵌入式应用程序生成MISRA C:2012兼容代码的可能性,以及符合CERT C, CWE, ISO/IEC TS 17961标准的代码。

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到

也看到处理不兼容的自动存根

在模型中发现整数溢出

要查看导致整数溢出的条件,请创建线束模型。当您模拟线束时,输入会复制错误。点击查看测试用例在Model Advisor报告中。

另请参阅

检测非有限和NaN浮点值

检查身份证mathworks.sldv.infnan

检测模型中的非有限和NaN浮点值

描述

该检查检测模型中出现的非有限和NaN浮点值。

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到

也看到处理不兼容的自动存根

在模型中找到的非有限和NaN浮点值

要查看导致出现非有限和NaN浮点值的条件,请创建线束模型。当您模拟线束时,输入会复制错误。点击查看测试用例在Model Advisor报告中。

另请参阅

检测非正常浮点值

检查身份证mathworks.sldv.subnormal

检测模型中的非正常浮点值

描述

此检查检测模型中出现的非正常浮点值。

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到

也看到处理不兼容的自动存根

在模型中发现非正常浮点值

要查看导致出现非正常浮点值的条件,请创建线束模型。当您模拟线束时,输入会复制错误。点击查看测试用例在Model Advisor报告中。

另请参阅

检测指定的最小值和最大值违规

检查身份证mathworks.sldv.minmax

检测超过指定最小值和最大值的信号

描述

该分析检查整个模型和输出端口上的中间信号的指定最小值和最大值(设计范围)。如果分析检测到信号超出了设计范围,那么结果将确定模型中错误发生的位置。

遵循此检查的建议增加了为嵌入式应用程序生成符合MISRA C:2012标准的代码的可能性,以及符合CERT C和CWE标准的代码。

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到

也看到处理不兼容的自动存根

违反了模型中的最小值和/或最大值

要查看导致冲突的条件,请创建一个线束模型。当您模拟线束时,输入会复制错误。点击查看测试用例在Model Advisor报告中。

另请参阅

检测数据存储访问违规

检查身份证mathworks.sldv.dsmaccessviolations

检测模型中的数据存储访问违规。

描述

该检查检测这些数据存储访问违规:

  • Read-before-write

  • Write-after-read

  • Write-after-write

结果和建议的行动

结果 建议的行动
失败,模型不兼容

解决模型不兼容问题。看到的:

发现数据存储访问违规

在Model Advisor报告中,单击查看测试用例。该软件创建一个线束模型和信号生成器块显示复制错误的测试用例。

另请参阅