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

获取试用版软件