## 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. | |

2 | Verify that your model is compatible with Simulink Design Verifier. | |

3 | Add a Proof Objective block to your model to prepare for its proof. | |

4 | Configure Simulink Design Verifier to prove properties. | |

5 | Prove a property of your model. | |

6 | Review the analysis results. | |

7 | Add proof assumptions to specify analysis constraints. | |

8 | Prove a property of the customized model and interpret the results. |

### 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

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

**Generate 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 items:

Signal Builder block named

`Inputs`

— A group of signals that falsify proof objectives.Subsystem block named

`Test Unit`

— A copy of your model.DocBlock named

`Test Case Explanation`

— A textual description of the counterexamples that the analysis generates.A Size-Type block — 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 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.

To simulate your harness model, on the

**Simulation**tab, click**Run**.The Simulink software simulates 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 Builder 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 the following 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. | Manage Simulink Design Verifier Data Files |

View the log file. | View Log 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.

In your model window, insert the Proof Assumption block between the Inport and Compare To Zero blocks.

In your model, double-click the Proof Assumption block to access its attributes.

The Proof Assumption block parameter 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 Proof Assumption block parameter 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.

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 or go to the top of the browser window 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 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.