Simulink Design Verifier 检查
Simulink Design Verifier 检查概述
这些检查可帮助您为Simulink® Design Verifier™分析准备模型。当您运行 Simulink Design Verifier 检查时，模型顾问会检查 Simulink Design Verifier 许可证。
有关模型顾问的更多信息，请参阅运行模型顾问检查 和 自动执行模型顾问检查 。
检查与 Simulink Design Verifier 的兼容性
检查 ID：mathworks.sldv.compatibility
识别Simulink Design Verifier分析不支持的元素。
描述
此项检查评估您的模型是否与 Simulink Design Verifier 兼容。
结果和建议的操作
| 条件 | 建议采取的操作 |
|---|---|
| 不相容 | 避免在您想要分析的模型或模型组件中使用以下不受支持的软件功能或 Simulink 模块： |
| 部分兼容 |
|
| 兼容的 | Simulink Design Verifier 可以分析你的模型。 |
另请参阅
检测死逻辑
检查 ID：mathworks.sldv.deadlogic
识别在仿真中保持非活动的逻辑。
描述
此项检查可识别模型中在仿真中保持非活动的部分。
您可以运行更详细的分析，使用Simulink Design Verifier设计错误检测来识别死逻辑和活动逻辑。有关更多信息，请参阅 检测由错误值导致的死逻辑 。
遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C 和 CWE 标准的代码的可能性
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅：
另请参阅 使用自动桩件处理不兼容性 。 |
| 模型中发现死逻辑 | Simulink Design Verifier证明了这些决策和条件结果不可能发生并且是模型中的死逻辑。死逻辑也可能是对参数指定约束或对输入端口指定最小和最大约束的副作用。在极少数情况下，Simulink Design Verifier 执行的近似计算可能会导致死逻辑。可能存在本次分析未确定的目标。为了扩展此分析的结果，请使用Simulink Design Verifier设计错误检测来识别活动逻辑。从 Simulink 编辑器中选择 App > Design Verifier > 设置 。在 配置参数窗格的 Design Verifier > 设计错误检测 窗格中，选择 死逻辑(部分) 或将 DVDetectDeadLogic 和 DVDetectActiveLogic 设置为 on 。 |
| 模型中未发现死逻辑 | Simulink Design Verifier未在模型中发现死逻辑。可能存在本次分析未确定的目标。为了扩展此分析的结果，请使用Simulink Design Verifier设计错误检测来识别活动逻辑。从 Simulink 编辑器中选择 App > Design Verifier > 设置 。在 配置参数窗格的 Design Verifier > 设计错误检测 窗格中，选择 死逻辑(部分) 或将 DVDetectDeadLogic 和 DVDetectActiveLogic 设置为 on 。 |
另请参阅
米斯拉C:2012：规则 2.1
证书 C，MSC07-C
CWE，CWE-561
Secure Coding (Embedded Coder)
hisl_0101: Avoid operations that result in dead logic to improve code compliance
检测超出范围的数组访问
检查 ID：mathworks.sldv.arraybounds
检测超出数组索引范围的访问操作
描述
此检查检测 Simulink Design Verifier 中超出边界的数组访问实例。
遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C、CWE、ISO/IEC TS 17961 标准的代码的可能性。
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅
另请参阅 使用自动桩件处理不兼容性 。 |
| 在模型中发现超出范围的数组访问 | 要查看导致越界数组访问的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。单击 Model Advisor 报告中的 查看测试用例。 |
另请参阅
米斯拉C:2012：规则 18.1
ISO/IEC TS 17961：2013，invptr
CERT C，ARR30-C
CWE, CWE-118
Secure Coding (Embedded Coder)
检测除以零
检查 ID：mathworks.sldv.divbyzero
检测模型中的除以零错误
描述
此检查可识别模型中除以零错误的操作。
遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C、CWE、ISO/IEC TS 17961 标准的代码的可能性。
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅
另请参阅 使用自动桩件处理不兼容性 。 |
| 在模型中发现除以零 | 要查看导致除以零的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。单击 Model Advisor 报告中的 查看测试用例。 |
另请参阅
米斯拉C:2012：指令 4.1
ISO/IEC TS 17961：2013年，潜水员
CERT C、INT33-C 和 FLP03-C
CWE、CWE-369
Secure Coding (Embedded Coder)
检测整数溢出
检查 ID：mathworks.sldv.integeroverflow
检测模型中的整数或定点数据溢出错误
描述
此检查可识别超出整数或定点运算的数据类型范围的运算。
遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C、CWE、ISO/IEC TS 17961 标准的代码的可能性。
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅
另请参阅 使用自动桩件处理不兼容性 。 |
| 模型中发现整数溢出 | 要查看导致整数溢出的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。单击 Model Advisor 报告中的 查看测试用例。 |
另请参阅
米斯拉C:2012：指令 4.1
ISO/IEC TS 17961：2013年，流入
CERT C、INT30-C 和 INT32-C
CWE、CWE-190
Secure Coding (Embedded Coder)
检测非有限和 NaN 浮点值
检查 ID：mathworks.sldv.infnan
检测模型中的非有限和 NaN 浮点值
描述
此检查可检测模型中非有限和 NaN 浮点值的出现情况。
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅
另请参阅 使用自动桩件处理不兼容性 。 |
| 在模型中发现非有限和 NaN 浮点值 | 要查看导致出现非有限和 NaN 浮点值的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。单击 Model Advisor 报告中的 查看测试用例。 |
另请参阅
检测低于正常的浮点值
检查 ID：mathworks.sldv.subnormal
检测模型中的次正常浮点值
描述
此检查可检测模型中是否出现低于正常的浮点值。
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅
另请参阅 使用自动桩件处理不兼容性 。 |
| 在模型中发现低于正常的浮点值 | 要查看导致出现低于正常值的浮点值的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。单击 Model Advisor 报告中的 查看测试用例。 |
另请参阅
检测指定最小值和最大值违规
检查 ID：mathworks.sldv.minmax
检测超出指定最小值和最大值的信号
描述
该分析检查整个模型的中间信号和输出端口上指定的最小值和最大值（设计范围）。如果分析检测到信号超出了设计范围，结果将确定模型中出现错误的位置。
遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C 和 CWE 标准的代码的可能性。
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅
另请参阅 使用自动桩件处理不兼容性 。 |
| 违反模型中的最小值和/或最大值 | 要查看导致违规的情况，请创建框架模型。当您仿真框架时，输入会复制错误。单击 Model Advisor 报告中的 查看测试用例。 |
另请参阅
米斯拉C:2012：指令 4.1
证书 C，API00-C
CWE，CWE-628
Secure Coding (Embedded Coder)
检测数据存储访问违规
检查 ID：mathworks.sldv.dsmaccessviolations
检测模型中的数据存储访问冲突。
描述
此项检查检测到以下数据存储访问冲突：
先读后写
读后写
写后写
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅：
|
| 发现数据存储访问违规 | 在 Model Advisor 报告中，点击查看测试用例 。该软件创建一个框架模型，并且Signal Editor模块显示复制错误的测试用例。 |
另请参阅
检测模块输入范围违规
检查 ID：mathworks.sldv.blockinputrangeviolations
检测模型中的模块输入范围违规。
描述
此检查检测具有以下设置的模块的输入范围违规：
对于这些模块，当 输入超出范围的诊断 参数设置为 警告 或 错误 时：
当 默认情况诊断 参数设置为 警告 或 错误 时，Multiport Switch 会阻塞。
当 逼近方法 参数设置为 CORDIC 时，Trigonometric Function 会阻塞
注意
当 插值方法 设置为 Akima 样条 或 三次样条 时，检查不会标记 n-D Lookup Table 模块的模块输入范围违规。
结果和建议的操作
| 结果 | 建议采取的操作 |
|---|---|
| 失败，模型不兼容 | 解决模型不兼容问题。请参阅：
|
| 发现模块输入范围违规 | 在 Model Advisor 报告中，点击查看测试用例 。该软件创建一个框架模型，并且Signal Editor模块显示复制错误的测试用例。 |
另请参阅
检查 rem 和倒数运算的用法
检查 ID：mathworks.sldv.hismviolationshisl_0002
描述
识别导致非有限结果的 rem 和 reciprocal 运算的使用情况。
结果和建议的操作
| 条件 | 建议采取的操作 |
|---|---|
模型或子系统包含可能导致非有限输出信号的 rem 或 reciprocal 操作。实时嵌入式系统不支持非有限信号。 | 当使用rem或reciprocal操作时，保护相应的输入不等于零。 |
另请参阅
检查 Sqrt 运算的使用情况
检查 ID：mathworks.sldv.hismviolationshisl_0003
描述
识别输入可以为负数的Sqrt运算。
结果和建议的操作
| 条件 | 建议采取的操作 |
|---|---|
| 模型中的一个或多个 Sqrt 操作的输入在仿真中可能会变为负值。 | 重塑以保护Sqrt操作的输入不会变为负值。 |
另请参阅
检查 log 和 log10 操作的使用情况
检查 ID：mathworks.sldv.hismviolationshisl_0004
描述
识别导致非有限结果的 log 和 log10 操作。
结果和建议的操作
| 条件 | 建议采取的操作 |
|---|---|
模型中使用的一个或多个 log 和 log10 操作可能需要非有限数支持，而实时嵌入式系统不支持这种支持。 | 考虑保护这些操作的输入，使其不小于或等于零。 |
另请参阅
检查互惠 Sqrt 模块的使用情况
检查 ID：mathworks.sldv.hismviolationshisl_0028
描述
识别输入可以为零或负数的 Reciprocal Sqrt 模块。
结果和建议的操作
| 条件 | 建议采取的操作 |
|---|---|
| 模型中的一个或多个 Reciprocal Sqrt 模块的输入在仿真中可以变为零或负值。 | 重新建模以保护Reciprocal Sqrt模块的输入不会变为负面。 |
另请参阅
You can also select a web site from the following list:
Americas
- América Latina (Español)
- Canada (English)
- United States (English)
Europe
- Belgium (English)
- Denmark (English)
- Deutschland (Deutsch)
- España (Español)
- Finland (English)
- France (Français)
- Ireland (English)
- Italia (Italiano)
- Luxembourg (English)
- Netherlands (English)
- Norway (English)
- Österreich (Deutsch)
- Portugal (English)
- Sweden (English)
- Switzerland
- United Kingdom (English)