标题

标题部分列出了以下信息：

目录

目录位于标题部分之后。单击目录中的项目可以快速导航到报告中的特定章节。

模型信息

模型信息部分提供有关模型当前版本的以下信息：

分析选项

分析选项部分提供有关Simulink Design Verifier分析设置的信息。

分析选项部分列出了影响Simulink Design Verifier分析的参数。如果您启用了覆盖率过滤，则过滤文件的名称将包含在此部分中。

不支持的模块

如果您的模型包含不受支持的模块，则默认情况下会启用自动桩件以允许分析继续。启用自动桩件后，软件仅考虑不受支持的模块的接口，而不考虑它们的实际行为。该技术使得软件能够完成分析。但是，如果任何不受支持的模型模块影响仿真结果，则分析可能只能获得部分结果。

仅当分析桩件不受支持的模块时，才会出现“不受支持的模块”部分；它在表中列出不受支持的模块，并带有指向模型中每个模块的超链接。

有关自动桩件的更多信息，请参阅 使用自动桩件处理不兼容性 。

用户工件

用户工件部分提供有关Simulink Design Verifier分析中的测试数据和覆盖率数据的信息。

参数和变量约束

参数和变量约束部分中的参数约束子部分提供了有关 Simulink Design Verifier 在模型分析期间应用的测试条件的信息。

您可以通过单击“约束”表中的超链接导航到模型中的约束。该软件会在模型窗口中突出显示相应的 Test Condition模块，并打开一个新窗口详细显示该模块。

您可以从约束表中的源和源类型列中查看有关约束的工作区信息。这些列包含有关参数是否来自模型工作区、基础工作区还是数据字典的信息。

模块替换摘要

模块替换摘要提供了 Simulink Design Verifier 执行的模块替换的概述。仅当 Simulink Design Verifier 替换模型中的模块时才会出现。

表格中的每一行对应于Simulink Design Verifier应用于模型的特定模块替换规则。下表列出了以下内容：

要在您的模型中找到特定的模块替换，点击表的“已替换的模块”列中该替换的名称；软件会在模型窗口中突出显示受影响的模块，并打开一个新窗口详细显示该模块。

近似值

近似值表的每一行描述了 Simulink Design Verifier 在模型分析过程中使用的一种特定类型的近似值。

分析框架信息

分析框架信息 部分概述了由 Simulink Design Verifier 生成的用于分析模型的分析框架。分析框架信息 部分根据模型是导出函数模型还是包含 Function Caller 模块而没有相应 Simulink 函数的模型来显示这些子部分。

出口功能分析时间表.  Simulink Design Verifier 假设在分析过程中有一个分析框架用于调用 Export Functions。例如，下表显示了模型sldvExportFunction_autosar_multirunnables 的分析框架：

用于分析的桩件 Simulink 函数.  用于分析的插桩 Simulink 函数 中的这个表列出了与分析框架中桩件的 Simulink 函数相对应的函数原型：

设计错误检测目标状态

如果您运行设计错误检测分析，Design Error Detection Objectives Status 部分可以包含以下目标状态的子部分：

• 死逻辑

• 近似下的死逻辑

• 主动逻辑 - 需要仿真

• 目标有效

• 近似下有效的目标

• 用反例来证伪目标

• 目标错误 - 需要仿真

如果在设计误差检测分析中使用了Observer Reference模块，那么本节将显示Observer 模型子节中的观察者信息和设计模型子节中的设计模型信息。当模型中不存在活动逻辑时，此部分将为空。

设计模型小节中的表格显示了sldvdemo_debounce_validprop示例模型中的活动逻辑列表。

Observer模型部分将不会显示任何报告的活动逻辑，因为在设计错误检测分析中忽略了观察者。

死逻辑.  死逻辑 部分列出了分析发现死逻辑的项目。

此图显示了 sldvdemo_fuelsys_logic_simple模型生成的分析报告的 死逻辑 部分。

近似下的死逻辑.  在逼近下为死逻辑 部分列出了分析发现在近似影响下存在死逻辑的模型项。

在 R2017b 之前的版本中，本节可以包含标记为 死逻辑 的目标。

此图显示了生成的分析报告的在逼近下为死逻辑部分。

主动逻辑 - 需要仿真.  活动逻辑 - 需要仿真 部分列出了分析发现活动逻辑的模型项。为了确认活动逻辑状态，您必须运行额外的测试用例仿真。

在 R2017b 之前的版本中，本节可以包含标记为 活动逻辑 的目标。

此图显示了 sldvdemo_fuelsys_logic_simple模型生成的分析报告的 活动逻辑 - 需要仿真 部分。

目标有效.  目标有效 部分列出了分析发现有效的设计错误检测目标。对于这些目标，分析确定所描述的设计错误不会发生。

在 R2017b 之前的版本中，本节可以包含标记为 Proven Valid 的目标。

此图显示了 sldvdemo_design_error_detection模型生成的分析报告的 目标有效 部分。

近似下有效的目标.  在逼近下有效的目标 部分列出了分析在近似影响下发现有效的设计错误检测目标。

在 R2017b 之前的版本中，本节可以包含标记为 Proven Valid 的目标。

此图显示了生成的分析报告的在逼近下有效的目标部分。

用反例来证伪目标.  用反例证伪的目标 列出了一组设计错误检测对象，这些对象的反例已经过仿真和验证，以观察报告的错误。

此图显示了 sldvdemo_design_error_detection模型生成的分析报告的 用反例证伪的目标 部分。

目标错误 - 需要仿真.  Objectives Error- Needs Simulation 部分列出了设计错误检测目标，分析发现了显示设计错误的测试用例。为了确认伪造状态，您必须运行额外的测试用例仿真。

在 R2017b 之前的版本中，本节可以包含标记为 证伪 的目标。

此图显示了 sldvdemo_array_bounds模型生成的分析报告的 Objectives Error - Needs Simulation 部分。

测试目标状态

如果您运行测试用例生成分析，Test Objectives Status 部分可以包含以下目标状态的子部分：

• 目标达成

• 目标满足 - 需求仿真

• 目标无法满足

• 近似下无法满足的目标

• 测试用例目标未定

当您分析将 模型覆盖率目标 设置为 增强的 MCDC 的模型时，软件会报告模型项目的检测状态。有关更多信息，请参阅 Simulink Design Verifier 中的增强 MCDC 覆盖范围 。

如果在测试用例生成分析中使用了Observer Reference模块，则每个测试目标状态部分将显示Observer 模型子部分中的观察者信息和设计模型子部分中的设计模型信息。如果在模型中未找到测试目标，则这些子部分将为空。

该表展示了sldvdemo_debounce_testobjblks示例模型中设计模型的部分满足的目标测试目标。

该表展示了sldvdemo_debounce_testobjblks示例模型中观察者模型的部分满足的目标测试目标。

目标达成.  满足的目标部分列出了分析满足的测试目标。生成的测试用例涵盖了目标。

此图显示了针对sldvdemo_fuelsys_logic_simple示例模型生成的分析报告的满足的目标部分。

目标满足 - 需求仿真.  满足的目标 - 需要仿真部分列出了分析满足的测试目标。为了确认满意状态，您必须运行额外的测试用例仿真。

在 R2017b 之前的版本中，本节可以包含标记为 满足 的目标。

此图显示了生成的分析报告的满足的目标 - 需要仿真部分。

目标无法满足.  未满足的目标部分列出了分析确定无法满足的测试目标。

在 R2017b 之前的版本中，本节可以包含标记为 Proven Unsatisfiable 的目标。

此图显示了针对sldvdemo_fuelsys_logic_simple示例模型生成的分析报告的未满足的目标部分。

近似下无法满足的目标.  在逼近下无法满足的目标 部分列出了分析过程中确定的由于近似而无法满足的测试目标。

在 R2017b 之前的版本中，本节可以包含标记为 Proven Unsatisfiable 的目标。

此图显示了生成的分析报告的在逼近下无法满足的目标部分。

测试用例目标未定.  根据测试用例未决的目标部分列出了由于分析过程中近似的影响而未确定的测试目标。

在 R2017b 之前的版本中，本节可以包含标记为 满足 的目标。

此图显示了针对sldvApproximationsExample示例模型生成的分析报告的根据测试用例未决的目标部分。

证明目标状态

如果您运行属性证明分析，Proof Objectives Status 部分可以包含以下目标状态的子部分：

• 目标有效

• 近似下有效的目标

• 用反例来证伪目标

• 目标被证伪——需要仿真

• 目标未定，有反例

如果在属性证明分析中使用了Observer Reference模块，则每个证明目标状态部分将在Observer 模型子部分中显示观察者信息，在设计模型子部分中显示设计模型信息。当模型中未发现任何目标时，这些小节将为空。

该表显示了sldvdemo_debounce_validprop示例模型中Observer模型的目标有效证明目标。

目标有效.  目标有效部分列出了分析认为有效的证明目标。

在 R2017b 之前的版本中，本节可以包含标记为 Proven Valid 的目标。

此图显示了针对sldvdemo_debounce_validprop示例模型生成的分析报告的目标有效部分。

近似下有效的目标.  在逼近下有效的目标 部分列出了分析在近似影响下发现有效的证明目标。

在 R2017b 之前的版本中，本节可以包含标记为 Objectives Proven Valid 的目标。

此图显示了生成的分析报告的在逼近下有效的目标部分。

用反例来证伪目标.  用反例证伪的目标部分列出了分析所反驳的证明目标。生成的反例表明违反了证明目标。

此图显示了针对sldvdemo_debounce_falseprop示例模型生成的分析报告的用反例证伪的目标部分。

目标被证伪——需要仿真.  证伪的目标 - 需要仿真部分列出了分析所反驳的证明目标。为了确认伪造的状态，您必须运行反例的额外仿真。

在 R2017b 之前的版本中，本节可以包含标记为 用反例证伪的目标 的目标。

此图显示了生成的分析报告的证伪的目标 - 需要仿真部分。

目标未定，有反例.  根据反例未决的目标 部分列出了由于分析过程中近似的影响而未确定的证明目标。

在 R2017b 之前的版本中，本节可以包含标记为 证伪 的目标。

此图显示了生成的分析报告的根据反例未决的目标部分。

目标未定状态

报告的此部分提供了有关模型分析过程中所有未确定目标的信息。

• 由于运行时错误，目标未确定

• 由于除以零，目标未定

• 由于非线性而未确定目标

• 由于桩件而未确定目标

• 由于数组超出范围，目标未定

• 目标未定

• 目标未定可能是由于反例过长

由于运行时错误，目标未确定.  对于证明目标和测试目标，由于运行时错误而未决的目标 部分列出了由于运行时错误而导致分析过程中未确定的目标。运行时错误发生在测试用例或反例的仿真中。

在 R2017b 之前的版本中，本节可以包含标记为 证伪 或 满足 的目标。

此图显示了生成的分析报告的由于运行时错误而未决的目标部分。

此示例向您展示如何查找当 Simulink® Design Verifier™ 返回状态为由于运行时错误而未定的目标时导致的错误。此前，Simulink® Design Verifier™并未解释错误原因的详细情况。

open_system('mUndecidedDueToRunTimeError');

由于除以零，目标未定.  对于所有类型的目标，由于除以零错误而未决的目标 部分列出了由于相关模型项目中的除以零错误而导致的分析过程中未确定的目标。要在对模型进行进一步分析之前检测除以零错误，请按照 检测整数溢出和除以零错误 中的步骤进行操作。

由于非线性而未确定目标.  对于所有类型的目标，由于存在非线性运算而未决的目标 部分列出了由于需要进行非线性算术计算而在分析过程中未确定的目标。Simulink Design Verifier 不支持非线性算术或非线性逻辑。

由于桩件而未确定目标.  对于所有类型的目标，由于插桩而未决的目标 部分列出了由于桩件而在分析过程中未确定目标的模型项目。在 R2013b 之前的版本中，这些目标可以包括标记为 Objectives Satisfied – No Test Case 或 Objectives Falsified – No Counterexample 的目标。

由于数组超出范围，目标未定.  对于所有类型的目标，由于数组越界而未决的目标 部分列出了由于相关模型项目中的数组范围错误而导致分析过程中未确定的目标。要检测模型中的超出范围数组错误，请参阅 检测超出范围的数组访问错误 。

目标未定.  对于所有类型的目标，目标未决 部分列出了分析无法在规定时间内确定结果的目标。

在这个属性证明的例子中，要么软件超出了其分析时间限制（由 最大分析时间 参数指定），要么您在软件完成处理这些目标之前中止了分析。

目标未定可能是由于反例过长.  某些设计错误（例如溢出）只有在非常长的测试用例中才会显现出来。这样的测试用例可能不可构建或仿真。如果 Simulink Design Verifier 检测到设计错误检查的反例过长，它会返回状态 Undecided Possibly Due to Long Counterexample 并给出该反例的最小长度，而不返回这样的反例。

本例中的模型计算 uint32 类型变量中布尔输入为真的次数。整数溢出是可能的，但只有当步数大于最大 unit32 值时才会发生。

open_system('counter');

目录

设计错误章节包含一个目录。目录中的每一项都是指向有关特定设计错误的结果的超链接。

概括

摘要部分列出了：

在下面的例子中，该软件分析了sldvdemo_debounce_falseprop模型以检测设计错误。分析检测到名为 Verify True Output 的验证子系统中的 Sum模块中存在溢出错误。

测试用例

测试用例部分列出了测试用例证伪设计错误目标的时间步和相应时间。Inport模块raw 的值为 255，这导致了溢出错误。

目录

测试用例章节包含目录。目录中的每一项都是指向特定测试用例信息的超链接。

概括

摘要部分列出了：

目标

目标部分列出：

生成的输入数据

对于与模型项相关的每个输入信号，生成的输入数据部分列出了测试用例实现特定测试目标的时间步和相应时间。如果信号值在这些时间步内没有改变，则表将时间步和时间列为范围。

预期输出

如果您在配置参数对话框的 Design Verifier > 结果窗格中选择 包括预期的输出值，则报告将包含每个测试用例的预期输出部分。对于与模型项相关的每个输出信号，该表列出了每个时间步的预期输出值。

长测试用例

如果将 测试套件优化 选项设置为 LongTestcases，则报告中的测试用例章节将包含较少的有关较长测试用例的部分。

目录

属性章节包含一个目录。目录中的每一项都是一个超链接，指向有关被伪造的特定属性的信息。

如果在属性证明分析中使用了Observer Reference模块，则每个属性章节将在Observer 模型子节中显示观察者信息，在设计模型子节中显示设计模型信息。当模型中没有属性时，它将为空。

该表显示了 sldvdemo_debounce_validprop 示例模型中观察者模型的一个属性。

概括

摘要部分列出了：

在下面的例子中，软件分析了 sldvdemo_cruise_control_verification模型以进行属性证明。分析证明，名为 BrakeAssertion 的 Assertion模块的输入非零。

反例

反例部分列出了反例证伪该属性的时间步和相应时间。本节还列出了该时间步的信号值。