探索分析模式在 Simulink Design Verifier

考虑一个简单的模型，它包括两个 Logical Operator 模块和一个 Memory 模块。该模型中的持久信息仅限于 Memory 模块的布尔值。该模型的输入是一个布尔值。

A simple model with two Logical Operator blocks and a Memory block. in represents input and out represents output.

下表描述了模型的完整行为，包括任意长的输入序列所产生的行为。

#	输入	内存值	XOR 模块的输出=下一个内存值	AND 模块的输出
1	`false`	`false`	`false`	`false`
2	`true`	`false`	`true`	`false`
3	`false`	`true`	`true`	`false`
4	`true`	`true`	`false`	`true`

测试用例生成分析

测试目标是生成导致 true 输出的测试用例。当输入为 true 时，会产生 true 输出，而 Memory 模块的输出为 true。测试用例生成遵循一条路径来达到这一条件，这取决于初始模型条件：

如果初始内存值为 true，测试用例为单时间步，其中输入为 true。
假设初始内存值为 false，则测试用例为两个时间步：
1. 输入值为 true，内存值为 false（第 2 行）。因此，XOR 模块的输出为 true，使得内存值为 true。
2. 现在输入值和内存值都是 true（第 4 行），输出为 true，分析达到测试目标。

无数个测试用例可以导致输出为真，并且无论状态值如何，输出都可以在变为真之前任意时间保持为假。当 Simulink^® Design Verifier™ 搜索时，它会返回遇到的第一个满足目标的测试用例。这种情况总是时间步长最少的仿真。有时您可能会发现这个结果不理想，因为它不切实际或不满足其他测试需求。

该示例中的相同基本原理也适用于属性证明和测试用例生成。在测试用例生成期间，选项参数明确指定搜索准则。例如，您可以指定 Simulink Design Verifier 查找所有模块输出的路径，或者仅查找导致模块输出为真的路径。

设计错误检测分析

在错误检测分析过程中，Simulink Design Verifier 确定了数据溢出或除以零错误可能发生和不能发生的目标。分析创建了测试用例来演示错误如何发生。

属性证明分析

在属性证明分析期间，您可以指定希望 Simulink Design Verifier 证明的功能需求或属性，例如，输出始终为真。如果搜索完成而没有找到违反属性的路径，属性被证明。如果软件发现输出为错误的路径，它会创建一个导致输出为错误的反例。