Simulink Design Verifier

主要特性

  • Polyspace® 和 Prover Plug-In® 形式化分析引擎
  • 死逻辑、整数和定点溢出、被零除与设计属性冲突的检测
  • 功能和安全需求建模的模块和函数
  • 根据功能需求和模型覆盖目标(包括条件、判定和修订的条件/判定 (MCDC))生成测试向量
  • 模型属性验证功能,能生成冲突示例以供分析和调试
  • 支持定点和浮点模型

Simulink Design Verifier 用于在 Simulink® 环境中进行模型分析。您不需要生成代码,就可以在早期验证设计并确认需求。因此,您可以在整个设计流程中执行验证和确认。使用 Simulink Design Verifier 进行模型分析是对仿真的一个补充,它能够将仿真结果用于形式化方法进行模型分析。

Simulink Design Verifier 支持通常用于嵌入式控制设计的 Simulink 与 Stateflow® 离散时间模型。

Design error detection in a model using Simulink Design Verifier.
在模型中使用 Simulink Design Verifier 进行设计错误检测。红色高亮显示的模块存在设计错误;绿色高亮显示的子系统已证实无错误。

基于模型的设计中的形式化方法

Simulink Design Verifier 使用由 Prover Technology 的 Prover Plug-In 所提供的形式化分析技术以及 MathWorks 的 Polyspace 形式化分析引擎。这些技术依赖严格的数学过程,搜索模型的可能执行路径以获得测试用例和反例。传统测试方法使用具体数值来表现测试场景和预期结果,而形式化分析技术使用系统行为模型来替代具体数值。系统行为模型可以包括模型测试方案和验证目标,描述预期和非预期的系统行为。通过行为模型执行的形式化分析与仿真方法互补,可以让您对模型有更加深入的了解。

使用形式化方法进行错误检测

与仿真中的语义检查或分析不同,Simulink Design Verifier 使用的形式化方法可以发现特定动态运行情况是否会发生以及在什么条件下发生。这些信息可用于改进设计以及设计需求, 或用于辅助仿真调试和验证。Simulink Design Verifier 可以检测到以下常见设计错误:整数溢出、被零除、死逻辑和断言冲突。

检测整数溢出和被零除

您可以使用 Simulink Design Verifier 中的设计错误检测模式来发现整数溢出和被零除。此分析会自动执行,不需要额外的用户输入。它会提供所有模块的所有信号的允许范围,引导您找出问题的根本原因。最后,您可以直接在模型中查看结果,或生成 HTML 报告。

模型中的模块会标记为绿色、黄色或红色。绿色表示已经被证明不会导致整数溢出或被零除。黄色表示无法产生确定分析结论或超出分析时限的情况。如果在模型执行路径中发现错误,该路径中所有可显示整数溢出和被零除的后续块都将标记为黄色。

红色模块表示存在设计错误。Simulink Design Verifier 会为红色模块生成测试用例,可在仿真或测试中重现问题。您可以在 Simulink 中直接调用该测试用例并运行仿真。

检测死逻辑

您可以在 Simulink Design Verifier 中使用测试生成模式来检测死逻辑,即经证明在模型执行过程中永远不会被激活的模型部分。死逻辑通常因设计错误或需求错误而导致。在代码生成过程中,死逻辑会导致死代码。单独使用仿真测试难以检测到死逻辑,因为即使在运行大量仿真之后,仍然难以证明特定行为无法被激活。

在测试分析结束时,会根据测试标准为模型标记颜色。包含无法在仿真中激活的逻辑的模型对象标记为红色;包含可在仿真中完全激活的逻辑的模型对象标记为绿色。Simulink Design Verifier 会生成可在仿真过程中重现死逻辑的测试用例。

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 会验证是否存在能触发断言的情况。例如,您可以构造以下断言,每当反推作动器被连接上且有某个飞行状态指示器为“true”时触发。当设定的断言被违反时,它会被突出显示为红色而且也会生成触发这个断言的测试向量。除了 Simulink 中提供的断言模块,Simulink Design Verifier 还提供了其他模块用来定义各种约束,进行模型分析,使您能够在运行仿真前全面分析模型行为并找出设计缺陷。

根据需求对设计进行验证

离散系统的功能需求通常是指对系统行为的明确陈述,包括预期行为和绝不能出现的行为。绝不能出现的行为被称为安全需求。

在 Simulink 中表达功能需求

要以形式化方式验证模型的行为是否符合这些要求,首先需要将需求陈述从人类语言转换为形式分析引擎所能理解的语言。Simulink Design Verifier 使您能够使用 SimulinkMATLAB® 函数和 Stateflow 来表达形式化需求。Simulink 中的每项需求都关联有一个或多个验证目标。这些验证目标用于报告设计是否满足功能和安全需求。

Simulink Design Verifier 提供了一组基础模块和函数,可用来定义各种验证目标。模块库包括用于测试目标、证明目标、断言、限制的模块和函数,以及一组用于在时态方面对验证目标进行建模的专用时态运算符。

您可以将各项需求及其相关的验证目标分组,并建立相应的模块库,可以独立于模型进行管理和查看。

Simulink Design Verifier library of property examples.
Simulink Design Verifier 属性验证库示例。

如果将 Simulink Design Verifier 与 Simulink Verification and Validation™ 中的需求管理界面结合使用,则可将这些用于捕捉需求和验证目标的模块和函数关联到 Simulink 之外的更上层的需求文档。

证明设计需求

当需求和验证目标在验证模型中定义后,可借助形式化方法将其用于证明设计的正确性。

要引导功能需求的验证,使系统运行于指定状态,您可以使用Test Objective模块和 MATLAB 函数来定义测试目标。在测试生成过程中,Simulink Design Verifier 将尝试查找满足所定义目标的有效测试用例。如果目标永远无法满足,则表示模型的功能无法满足这一组指定的分析约束。

要根据安全需求验证设计的正确性,您可以使用Proof Objective模块和 MATLAB 函数来定义证明 目标。
在分析过程中,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、MATLAB 函数和 Stateflow 表示的设计需求可与模型同时进行仿真。您也可以在 SIL 模式或 PIL 模式下用它来验证生成的代码。模型覆盖率分析工具可收集仿真过程中验证目标的激活信息,并将覆盖率结果显示在 Simulink Design Verifier 的覆盖率报告中。您可以使用Proof Objective 模块来定义安全需求,并设置在出现冲突时停止仿真,从而加速根本原因分析和调试。

模型覆盖率分析

Simulink Design Verifier 可分析 SimulinkStateflow 模型中的算法和逻辑,生成测试用例和参数,以满足各种行业标准对于开发高完整性系统的要求。结构化覆盖标准的测试生成包括条件、判定和修改的条件/判定覆盖率 (MC/DC)。

生成测试

针对模型覆盖率生成的测试扩展了基于需求的测试。后者通过手工创建或在整个系统的仿真过程中收集而来。Simulink Design Verifier 采集现有的模型覆盖率信息,生成新的测试向量,补充所有在基于需求的测试过程中未满足的覆盖率目标。

Visual display of a generated test vector that activates previously untested functionality.

图示了一组测试向量,可测试之前未测试到的功能。

您可以使用这些测试向量来更好地理解缺失的需求并创建更完整的测试框架。为了简化带有大量输入和输出的模型的测试,Simulink Design Verifier 可识别未使用的信号并自动将其从测试框架中删除。

所有生成的测试向量都会保存为 MATLAB 结构体,可直接在模型仿真、SIL 或 PIL 测试中做为输入。采集的测试数据也可用于生成测试框架模型。

验证生成的测试向量

要验证生成的测试向量满足结构化覆盖率标准,您可以使用 Simulink Verification and Validation 中提供的模型覆盖率分析工具。它会监控仿真并衡量形式化分析过程中报告的目标是否已达到。除了条件、决策和 MC/DC 覆盖率的覆盖目标,模型覆盖率分析工具还会报告测试目标、证明 目标、假设、约束、查表的覆盖率,并记录仿真过程中的信号范围。

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

分析生成代码的测试覆盖率

Simulink Design Verifier 提供了测试自动化功能,在 SIL 和 PIL 模式下自动化执行生成的测试用例来检测代码。Simulink Design Verifier 中的代码验证功能需要使用 Embedded Coder™。在文本执行过程中,您可以借助 Embedded Coder 中提供的代码覆盖率分析工具来收集代码覆盖率信息。

Designing Supervisory Control for Safety-Critical Systems

观看网上技术交流会录像