Learn more about Simulink Design Verifier

Analyzing a Simple Model

This simple Simulink model includes two Logical Operator blocks and a Memory block.

The persistent information in this model is limited to the Boolean value of the Memory block. The input to the model is a single Boolean value. The following table describes the complete behavior of the model, including the behavior that would result from an arbitrarily long sequence of inputs.

#	Input	Memory Value	Output of XOR Block = Next Memory Value	Output of AND Block
1	false	false	false	false
2	true	false	true	false
3	false	true	true	false
4	true	true	false	true

Suppose you want to generate test cases that result in a true output; this goal is your test objective. If you run the Simulink Design Verifier software to generate test cases that result in a true output, the software searches this table to see if such a scenario is possible.

After the Simulink Design Verifier software discovers a configuration that satisfies the test objective (in this case, when both the input and the Memory block output are true), it needs to find a path to reach this configuration from the initial conditions. If the initial memory value is true, the test case only needs to be a single time step (row 4) where the input was true.

If the initial memory value is false (the default), the test case must force the memory value to be true. In this example, the path requires two steps:

1. The input value is true and the memory value is false (row 2). Thus, the output of the XOR block is true, making the memory value true.

2. Now that the input value and memory value are both true (row 4), the output is true, so the analysis achieves the specified test objective.

An infinite number of test cases can cause the output to be true, and regardless of the state value, the output can be held false for an arbitrary time before making it true. When the Simulink Design Verifier software searches, it returns the first test case it encounters that satisfies the objective. This case is invariably the simulation with the fewest time steps. Sometimes you may find this result undesirable because it is unrealistic or does not satisfy some other test requirement.

The same basic principles from this example apply to property proving and test case generation. During test case generation, option parameters explicitly specify the search criteria. For example, you can specify that Simulink Design Verifier software find paths for all outputs or find only those paths that make where the output is true.

During property proving, you specify a functional requirement, or property, that you want the Simulink Design Verifier software to prove, for example, that the output is always true. If the search completes without finding a path that violates the property, the proof of that property completes successfully. If the software finds a path where the output is false, it creates a counterexample that causes the output to be false.

Model Analysis with Simulink Design Verifier Software

Analyzing Large Models

© 1984-2009- The MathWorks, Inc.    -   Site Help   -   Patents   -   Trademarks   -   Privacy Policy   -   Preventing Piracy   -   RSS