Main Content

Prove Properties in Large Models

Property proving uses the same underlying techniques as design error detection and test generation and suffers from the same performance limitations. However, unlike design error detection or 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 thorough proof requires that Simulink® Design Verifier™ 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.

There are two techniques you can use to improve the performance of property proving in a large model:

Find Property Violations While Designing Your Model

Simulink Design Verifier software offers a strategy that quickly identifies property violations in larger, more complicated models. While designing your model, analyze your model using this strategy so that you can fix any property violations before finalizing your design.

To identify property violations of a model, on the Design Verifier > Property Proving pane of the Configuration Parameters dialog box, specify the value of the Strategy parameter as FindViolation. 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.

During analysis, the software searches only for property violations within the specified number of time steps. By identifying and fixing the property violations first, you improve the performance of a property-proving analysis that uses the Prove strategy.

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.

Combine Proving Properties and Finding Proof Violations

Use the following technique for proving properties in large model. This technique 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 trivial counterexamples exist — 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 FindViolation, 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 required 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.