Main Content

本页采用了机器翻译。点击此处可查看英文原文。

分析简单模型

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 模块的输出
1falsefalsefalsefalse
2truefalsetruefalse
3falsetruetruefalse
4truetruefalsetrue

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