分析简单模型

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

这个简单的模型包括两个Logical Operator模块和一个Memory模块。该模型中的持久信息仅限于Memory模块的布尔值。该模型的输入是一个布尔值。下表描述了模型的完整行为，包括任意长的输入序列所产生的行为。

#	输入	记忆值	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 确定了数据溢出或除以零错误可能发生和不能发生的目标。分析创建了测试用例来演示错误如何发生。

分析简单模型

WeChat