分析简单模型
这个简单的模型包括两个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
,则测试用例为两个时间步:输入值为
true
,内存值为false(第2行)。因此,XOR模块的输出为true
,使得内存值为true
。现在输入值和内存值都是
true
(第 4 行),输出为true
,分析达到测试目标。
无数个测试用例可以导致输出为真,并且无论状态值如何,输出都可以在变为真之前任意时间保持为假。当 Simulink® Design Verifier™ 搜索时,它会返回遇到的第一个满足目标的测试用例。这种情况总是时间步长最少的仿真。有时您可能会发现这个结果不理想,因为它不切实际或不满足其他测试需求。
该示例中的相同基本原理也适用于属性证明和测试用例生成。在测试用例生成期间,选项参数明确指定搜索准则。例如,您可以指定 Simulink Design Verifier 查找所有模块输出的路径,或者仅查找导致模块输出为真的路径。
在属性证明分析期间,您可以指定希望 Simulink Design Verifier 证明的功能需求或属性,例如,输出始终为真。如果搜索完成而没有找到违反属性的路径,属性被证明。如果软件发现输出为错误的路径,它会创建一个导致输出为错误的反例。
在错误检测分析过程中,Simulink Design Verifier 确定了数据溢出或除以零错误可能发生和不能发生的目标。分析创建了测试用例来演示错误如何发生。