Simulink® Design Verifier™

Techniques for Proving Properties of Large Models

Property proving uses the same underlying techniques as test generation and suffers from the same performance limitations. However, unlike test generation, you often cannot simplify the problem without compromising the validity of the results.

You can quickly prove simple proof objectives that are not affected by model dynamics. However, a successful proof requires that the Simulink Design Verifier software search through all reachable configurations of your model—even the ones that are reached only after long time delays. The computation time and memory required to search a model completely often make an exhaustive proof impractical.

Simulink Design Verifier software offers a bounded model-checking capability to examine properties in larger, more complicated models. Bounded model checking restricts the search for property violations to a predefined limit of time steps. If a violation is not detected, it is impossible to violate the property with any input sequence having fewer time steps than the specified limit. However, you cannot prove that the property is true because there might be a counterexample within more time steps than the specified limit.

To configure the software for bounded model checking, on the Design Verifier > Property Proving pane of the Configuration Parameters dialog box, specify the value of the Strategy parameter as Find violation. When you use this strategy, the Maximum violation steps parameter becomes active so that you can specify an upper bound for the number of time steps in the search.

Note   For more information about the parameters for property proving, see Property Proving Pane.

Use the following technique for proving properties in large model combines proving and searching for violations:

1. On the Design Verifier > Property Proving pane, set the Strategy parameter to Prove.

2. On the Design Verifier pane, use a relatively short value for the Maximum analysis time parameter, such as 5–10 minutes. If there are trivial counterexamples—or if your properties do not depend on model dynamics—the analysis should complete in that amount of time.

3. Change the Strategy parameter to Find violation, and choose a small bound for the Maximum violation steps parameter, such as 4, 5, or 6. If your properties have simple counterexamples, the software should discover them.

4. If you do not find any violations with a small bound, increase the bound and look for longer counterexamples.

   1. Increase the bound in several increments, and observe the processing time and memory consumption. System resources might limit the length of violation that can be searched.

   2. In addition, consider the dynamics of your model and the number of time steps needed to transition between an arbitrary pair of configurations. If you choose too large a bound, the violation search can be more complex than the unbounded proof.

5. If you can run violation searches with relatively large bounds, e.g., 30–50 time steps, switch back to the Prove strategy, and use a longer time limit, such as several hours.

Handling Problems with Counters and Timers

Function Reference