Prove Properties in a Model

About This Example

The following sections describe a Simulink^® model, for which you prove a property that you specify using a Proof Objective block. This example demonstrates the property-proving capabilities of Simulink Design Verifier™.

In this example, you perform the following tasks.

Task	Description	See...
1	Construct the example model.	Construct Example Model
2	Verify that your model is compatible with Simulink Design Verifier.	Check Compatibility of Example Model
3	Add a Proof Objective block to your model to prepare for its proof.	Instrument Example Model
4	Configure Simulink Design Verifier to prove properties.	Configure Property-Proving Options
5	Prove a property of your model.	Analyze Example Model
6	Review the analysis results.	Review Analysis Results
7	Add proof assumptions to specify analysis constraints.	Customize Example Proof
8	Prove a property of the customized model and interpret the results.	Reanalyze Example Model

Construct Example Model

Construct a Simulink model to use in this example:

Create an empty Simulink model.
Copy the following blocks into your empty model window:
- From the Sources library, an Inport block to initiate the input signal whose value Simulink Design Verifier controls
- From the Logic and Bit Operations library, a Compare To Zero block to provide simple logic
- From the Sinks library, an Outport block to receive the output signal
Connect these blocks such so your model appears similar to the following model:
On the Modeling tab, click Model Settings.
On the Configuration Parameters dialog box, in the Solver pane, in the Solver selection:
- Set the Type option to Fixed-step.
- Set the Solver option to Discrete (no continuous states).
The Simulink Design Verifier can analyze only models that use a fixed-step solver.
Click OK to save your changes and close the Configuration Parameters dialog box.
Save your model with the name ex_property_proving_example_basic.

Check Compatibility of Example Model

Every time Simulink Design Verifier software analyzes a model, before the analysis begins, the software performs a compatibility check. If your model is not compatible, the software cannot analyze it.

You can also make sure you model is compatible with Simulink Design Verifier before you start the analysis:

Open the ex_property_proving_example_basic model.
On the Design Verifier tab, click Check Compatibility.
The Simulink Design Verifier software displays the log window, which states whether or not your model is compatible.
The model you just created is compatible.

What If a Model Is Partially Compatible?

If the compatibility check indicates that your model is partially compatible, your model contains at least one object that Simulink Design Verifier does not support. You can analyze a partially compatible model, but, by default, unsupported objects are stubbed out. The results of the analysis may be incomplete. For detailed information about automatic stubbing, see Handle Incompatibilities with Automatic Stubbing.

Instrument Example Model

Prepare your example model so that you can prove its properties with Simulink Design Verifier. Specifically, instrument the model by adding and configuring a Proof Objective block:

In the MATLAB^® Command Window, enter sldvlib.
The Simulink Design Verifier library appears.
Open the Objectives and Constraints sublibrary.
Copy the Proof Objective block to your model and insert it between the Compare To Zero and Outport blocks.
In your model, double-click the Proof Objective block.
The Proof Objective block parameters dialog box opens.
In the Values box, enter 1.
The Simulink Design Verifier software will attempt to prove that the signal output by the Compare To Zero block always attains this value for any signals that it receives.
Click OK to apply your changes and close the Proof Objective block parameters dialog box.
Save your model and keep it open.

Configure Property-Proving Options

Configure Simulink Design Verifier to prove properties of the ex_property_proving_example_basic model that you instrumented:

Open the ex_property_proving_example_basic model.
On the Design Verifier tab, in the Mode section, select Property Proving.
Click Property Proving Settings.
Click OK to apply your changes and close the Configuration Parameters dialog box.
Note
On the Property Proving pane, you can optionally specify values for other parameters that control how Simulink Design Verifier proves properties of your model. For more information, see Design Verifier Pane: Property Proving.
Save the ex_property_proving_example_basic model.

Analyze Example Model

To analyze the ex_property_proving_example_basic model, on the Design Verifier tab, click Prove Properties. Simulink Design Verifier begins a property-proving analysis.

During the analysis, the log window shows the progress of the analysis. It displays information such as the number of objectives processed and which objectives were satisfied or falsified.

To terminate the analysis at any time, in the log window, click Stop.

Review Analysis Results

When the analysis is complete, the log window displays the following options for reviewing the results:

Highlight the analysis results on the model
Generate a detailed HTML analysis report
Create a harness model with test cases
Simulate the test cases created by the model and produce a model coverage report

You can also view the Simulink Design Verifier data file. For detailed information about the data file, see Manage Simulink Design Verifier Data Files.

The following sections describe how you can review the analysis results:

Review Results on Model
Review Detailed Analysis Report
Review Harness Model
Simulate Model with Counterexample
Review Analysis Results

Review Results on Model

You can review the analysis results at a glance by viewing the blocks that are highlighted in the model window. The highlighting can have four colors:

Green — The analysis proved all the proof objectives valid.
Red — The analysis disproved a proof objective and generated a counterexample that falsified that objective.
Orange — The analysis disproved a proof objective, but it could not generate a counterexample or the proof objective remained undecided. This result occurs due to:
- A proof objective on a signal whose value the software cannot control, for example, a Constant block
- A proof objective that depends on nonlinear computation
- A proof objective that creates an arithmetic error, such as division by zero
- Automatic stubbing being enabled, and the analysis encountering an unsupported block whose operation it does not understand but that the analysis requires to generate the counterexample
- The analysis timing out
- Limitations of the analysis engine
Gray — The model object was not part of the analysis.

Highlight the analysis results on the example model:

In the Results Summary window for the ex_property_proving_example_basic analysis, click Highlight analysis results on model.
The Proof Objective block is highlighted in red, which indicates that a proof objective was falsified with a counterexample.
The Simulink Design Verifier Results window appears.
As you click objects in the model, this window changes to display detailed analysis results for that object.
Tip
By default, the Simulink Design Verifier Results window is always the topmost visible window. To allow the window to move behind other window, click and clear Always on top.
Click the highlighted Proof Objective block.
The Simulink Design Verifier Results window indicates that the proof objective that the output signal from the Compare to Zero was not 1 was disproved with a counterexample.

Review Detailed Analysis Report

To create a detailed HTML analysis report:

In the Simulink Design Verifier Results Summary window, click HTML to view detailed analysis report.
The HTML report opens in a browser window.
The report includes the following Table of Contents. Click a hyperlink to navigate to particular section in the report.
In the Table of Contents, click Summary.
The Summary provides an overview of the analysis results, and it indicates that Simulink Design Verifier identified a counterexample that falsifies an objective in your model.
In the Table of Contents, click Proof Objectives Status.
The Objectives Falsified with Counterexamples table lists the proof objectives that Simulink Design Verifier disproved using a counterexample that it generated. You can locate the objective in your model window by clicking Proof Objective; the software highlights the corresponding Proof Objective block in your model window.
In the Objectives Falsified with Counterexamples table, under the Counterexample column, click 1.
This section displays information about proof objective 1 and provides details about the counterexample that Simulink Design Verifier generated to disprove that objective. In this counterexample, a signal value of 99 falsifies the objective that you specified using the Proof Objective block. That is, 99 is not less than or equal to 0, which causes the Compare To Zero block to return 0 (false) instead of 1 (true).

Review Harness Model

Create a harness model with counterexamples that falsify the proof objectives in your model:

In the Simulink Design Verifier log window, click Create harness model.
The software creates a harness model named ex_property_proving_example_basic_harness.
The harness model contains the following blocks:
- A Signal Editor block named Inputs — A group of signals that falsify proof objectives.
- A Subsystem block named Test Unit — A copy of your model.
- A DocBlock named Test Case Explanation — A textual description of the counterexamples that the analysis generates.
- A Size-Type — A subsystem that transmits signals from the Inputs block to the Test Unit block. This block verifies that the size and data type of the signals are consistent with the Test Unit block.
Double-click the Inputs block. The Block Parameters dialog box opens. Click the Open Signal Editor button to open the Signal Editor dialog box.
The input signal 1 causes the output of the Compare to Zero block to be 0. This counterexample violates the proof objective that specifies that the output of the Compare to Zero block be 1.

Simulate Model with Counterexample

Simulate the harness model to observe the counterexample that falsifies the proof objective in your model:

Open the ex_property_proving_example_basic model.
On the Simulation tab, click Library Browser.
From the Sinks library, copy a Scope block into your harness model window. The Scope block allows you to see the value of the signal output by the Compare To Zero block in your model.
In your harness model window, connect the output signal of the Test Unit subsystem to the Scope block.
Simulate the harness model.
In your harness model window, double-click the Scope block to open its display window.
The Scope block displays the value of the signal output by the Compare To Zero block in your model. In this example, the Compare To Zero block returns 0 (false) throughout the simulation, which falsifies the proof objective that the output of the Compare to Zero block be 1 (true). The counterexample that the Signal Editor block supplies falsifies the proof objective.

Review Analysis Results

As long as your model remains open, you can view the results of your most recent Simulink Design Verifier analysis results in the Results Summary window.

On the Design Verifier tab, in the Review Results section, click Results Summary. The Results Summary window opens displaying the results of the latest Simulink Design Verifier analysis.

For any Simulink Design Verifier analysis, from the Results Summary window, you can perform these tasks.

Task	For more information
Highlight the analysis results on the model.	Highlight Results on the Model
Generate a detailed analysis report.	Review Results
Create the harness model, or if the harness model already exists, open it. If no counterexamples were created during the analysis, this option is not available.	Manage Simulink Design Verifier Harness Models
View the data file and Log file.	Manage Simulink Design Verifier Data Files

After you close your model, you can no longer view the analysis results.

Customize Example Proof

Modify the simple Simulink model whose proof objective Simulink Design Verifier disproved in the previous task. Specifically, customize the proof by adding and configuring a Proof Assumption block:

In the MATLAB Command Window, type sldvlib.
The Simulink Design Verifier library opens.
Open the Objectives and Constraints sublibrary.
Copy the Proof Assumption block to your model.
Insert the Proof Assumption block between the Inport and Compare To Zero blocks.
Double-click the Proof Assumption block to access its attributes.
The Block Parameters dialog box opens.
In the Values box, enter [-1, 0]. When proving properties of this model, Simulink Design Verifier constrains the signal values entering the Compare To Zero block to the specified range. If the input to the Compare to Zero block is always within this range, the output of the Compare to Zero block will always be 1.
Click Apply and then OK to apply your changes and close the Block Parameters dialog box.
Save the ex_property_proving_example_basic model and keep it open.

Reanalyze Example Model

Analyze the model that you modified to see how the Proof Assumption block affects the property-proving analysis.

Open the ex_property_proving_example_basic model. On the Design Verifier tab, click Prove Properties.

When the analysis is complete, the log window displays the options. There is no option to create a harness model because the analysis satisfied all proof objectives in your model, so there are no counterexamples.

Review Results of Second Analysis

Review the results of the second analysis.

Review Results on the Model

Highlight the model to see the analysis results:

Click Highlight analysis results on model.
The Proof Objective is now highlighted in green.
Click the Proof Objective block.
The Simulink Design Verifier Results window shows that the proof objective that states that the signal be 1 is valid.

Review Analysis Report

Review the analysis results in the detailed report:

Click Generate detailed analysis report.
In the Table of Contents, click Summary.
The Summary chapter indicates that Simulink Design Verifier proved a proof objective in the model.
Scroll to the Constraints section. The Constraints section lists the analysis constraint you specified in the Proof Assumption block.
Scroll back to the top of the browser window. In the Table of Contents, click Proof Objectives Status.
The Objectives Proven Valid table lists the proof objectives that Simulink Design Verifier proved to be valid.
Scroll down to view the Properties chapter and in the Table of Contents, click Properties.
The Proof Objective summary indicates that Simulink Design Verifier proved an objective that you specified in your model. The Proof Assumption block restricts the domain of the input signals to the interval [-1, 0]. Therefore, the software proves that this interval does not contain values that are greater than zero, thereby satisfying the proof objective.

Analyze Contradictory Models

If the analysis produces the error The model is contradictory in its current configuration, the software detected a contradiction in your model and it cannot analyze the model. You can have a contradiction if your model has Proof Assumption blocks with incorrect parameters. For example, an assumption could state that a signal must be between 0 and 5 when the signal is constant 10.

If the software detects a contradiction, all previous results are invalidated and the software reports that all the properties are falsified.

Note

Constraints added at the inputs either through design minimum/maximum or test conditions/proof assumptions do not lead to a contradiction. However, if you constrain signals that are downstream of a computation by using test conditions/proof assumptions, you must ensure that the constrained condition is feasible through the model computation. Otherwise, the resulting model is contradictory that may produces invalid results with or without an explicit analysis error. To ensure that the constraints are feasible, first try the same condition using a Test Objective. If it can be satisfied, you can use the same condition safely as a constraint.

Prove Properties in a Large Model

A thorough proof of your model 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.

Prove Properties in Large Models gives detailed information about strategies you can use to improve the performance of a property-proving analysis of a large model.