Accelerating the pace of engineering and science

Simulink Design Verifier

主要特性

  • 根据功能需求和模型覆盖目标(包括条件、决策和 MCDC)生成测试用例输入
  • 检测死逻辑、整数和定点溢出、数组访问越界、被零除以及违反设计需求
  • 验证根据功能和安全需求建模的模块
  • 属性证明功能,能生成冲突示例以供分析和调试
  • 用于分析大型模型中功能依赖关系和问题行为的 Model Slicer
  • 用于定点和浮点模型的 Polyspace® 和 Prover® 形式化验证引擎

Simulink Design Verifier 概述
Identify design errors, generate test cases, and verify designs against requirements using Simulink Design Verifier™.

Simulink Design Verifier™ 可让您尽早确认您的设计并验证需求,无需生成代码。它可以帮助提高您的设计在 Simulink® 环境中的稳健性。您可以使用在数学上严格的形式化方法分析控制逻辑、S-函数和 MATLAB® 代码。与测试场景和预期结果采用具体数据值表示的传统测试方法不同,形式化验证技术可改为使用系统行为模型。形式化验证可以证明软件的某些属性,如软件是否包含运行时错误,让您对系统需求有更深入的了解。

设计错误检测

Simulink Design Verifier 可以发现特定的动态执行场景是否会发生以及在什么条件下发生。您可以检测以下设计错误:整数溢出、被零除、死逻辑和数组越界。在设计周期的早期阶段,在执行基于仿真的测试之前发现这些错误,可以防止以后代价高昂的修复工作。

Design error detection in a model using Simulink Design Verifier.
设计错误检测。以红色突出显示的块具有设计错误;以绿色突出显示的子系统经验证是正确的。

设计错误检测是完全自动的,您可以直接在模型中或在 HTML 报告中评审结果。提供了所有块上所有信号的允许范围,可指导您找到问题的根源。在该模型中,块被标记为绿色、橙色或红色:绿色表示没有检测到错误,橙色表示分析在既定时间没有得出确定的结果,红色表示出现设计错误的块。Simulink Design Verifier 自动生成测试用例输入,为每个红色块重新制造错误场景。您可以在 Simulink 中使用这些测试输入,理解并调试发生错误的条件。

死逻辑检测

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
死逻辑检测,Simulink Design Verifier 用红色突出显示了 Stateflow 图中的跳转。此跳转发生死逻辑是因为“press < zero_thresh”条件决不能为 false。

死逻辑检测模式在模型中查找已经过时的或者在执行过程中不活动的对象。死逻辑通常由设计或需求错误导致。在代码生成过程中,死逻辑会导致死代码。包含的逻辑在仿真中不能激活的模型对象被标记为红色;包含的逻辑在仿真中能够完全激活的模型对象被标记为绿色。仅通过在仿真中测试很难检测死逻辑,因为即使在运行大量仿真之后,也难以证明特定的行为无法被激活。

测试用例输入生成

仅验证实现模型的输入输出行为并不能保证设计的正确性。功能测试是模型验证的重要的第一步,但这些测试从本质上讲是从需求派生的,可能不完整。要提高设计的稳健性,可以使用结构化验证技术(如模型覆盖),帮助识别模型中未使用的仿真路径。从本质上讲,模型覆盖是对测试用例执行模型功能的完整性的一种测量,可以告诉您测试用例执行的路径的百分比。通过调查未经测试的路径,您可以检测潜在的设计错误。

扩展现有测试用例以实现模型的全面覆盖
利用现有测试用例并使用形式化方法对 Simulink Design Verifier™ 中生成的测试实现全覆盖。

Simulink Design Verifier 结合形式化方法和启发式技术,生成实现模型覆盖和自定义用户准则的测试用例。为模型覆盖而生成测试用例,增加和扩展了手动创建的或在完整的系统仿真过程中收集的基于需求的测试输入。除了用于条件、决策和 MCDC 覆盖的覆盖目标外,还可以指定用来生成基于需求的测试用例的自定义测试目标。

基于需求的测试
使用 Simulink Design Verifier™ 从系统需求模型生成测试用例。

您可以使用 Test Generation Advisor 为测试生成选择模型组件(自动子系统和模型块)。Generation Advisor 执行高级分析,帮助您在测试生成之前更好地了解您的模型,尤其是大型模型、复杂模型或者不确定测试生成兼容性的模型。所有生成的测试用例输入都作为一个 MATLAB 结构体进行捕获,可在仿真、SIL 或 PIL 的测试执行中直接用做输入。采集的测试数据还可用于 Simulink Test™ 和相关的测试框架。在测试执行过程中,您可以集成 Embedded Coder® 中提供的第三方代码覆盖工具,用于采集代码覆盖。

Simulink Design Verifier 经过 TÜV SÜD 认证,可用于必须符合 ISO 26262IEC 61508EN 50128 标准的开发过程。

Visual display of a generated test vector that activates previously untested functionality.
Test Generation Advisor:分层视图中模型和模型组件的测试生成兼容性、覆盖目标和死逻辑的概要。

使用 Model Slicer 隔离有问题的行为

Simulink Design Verifier 使用动态和静态分析的组合来追踪依赖关系,隔离模型中感兴趣的行为。依赖性分析包括确定块、信号和模型组件的依赖关系。对于具有较多层级和设计复杂的大型模型,这是一个漫长的过程。Model Slicer 可以帮助您了解模型的哪一部分影响特定的行为。使用静态分析,您可以识别所有可能的仿真路径的模型依赖关系;而使用基于仿真的分析,仅突出显示仿真过程中活动状态的路径。

依赖性分析从起点向上游、下游或双向传播。您可以高亮和跟踪端口、信号和块的功能依赖关系,将大型模型切割成更小的、独立的模型进行分析。还可以查看影响子系统输出的块,并通过多个开关和逻辑块跟踪信号路径。

Testing and debugging complex models
测试和调试复杂模型。确定模型中的关注区域,并生成切片模型,以供进一步分析和调试。

基于需求的验证

要根据特定功能或安全需求从形式上验证设计行为,需求语句首先需要从人类语言转换为形式化分析引擎可以理解的语言。Simulink Design Verifier 可让您使用 MATLAB 函数、Simulink 和 Stateflow® 表达形式化需求。Simulink 中的每个需求有一个或多个与之关联的验证目标。一旦捕获需求和验证目标,便可使用形式化方法来证明设计的正确性。

例如,在飞行跟踪系统中,您可以构建一个断言或证明目标,每当反推装置执行机构介入并且飞行状态指示器的值为“true”时就会触发。Simulink Design Verifier 会检查可能导致意外行为的所有可能的输入条件,然后报告检查结果。对于给定的证明目标,该设计可能被证明有效,也可能会发现其违反安全需求。当检测到违规时,Simulink Design Verifier 将生成一个可以在仿真中演示违规的测试用例。

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
根据用证明目标表示的安全需求验证设计的 Simulink Design Verifier 报告。该报告显示了一个证明设计有效的目标列表和一个分析发现反例的目标列表。

在结合使用 Simulink Design Verifier 和 Simulink Verification and Validation™ 中的需求管理界面时,您可以将用于捕获需求和验证目标的块和函数链接到 Simulink 外部更高层次的文本需求。