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.
Construct the example model.
Verify that your model is compatible with Simulink Design Verifier.
Add a Proof Objective block to your model to prepare for its proof.
Configure Simulink Design Verifier to prove properties.
Prove a property of your model.
Review the analysis results.
Add proof assumptions to specify analysis constraints.
Prove a property of the customized model and interpret the results.
Construct a Simulink model to use in this example:
Create an empty Simulink model.
Copy the following blocks into your empty model window:
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
Set the Solver option to
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
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:
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.
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.
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
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
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.
Design Verifier to prove properties of
ex_property_proving_example_basic model that
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.
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.
To analyze the
ex_property_proving_example_basic model, on the
Design Verifier tab, click Prove
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.
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 Simulink Design Verifier Data Files.
The following sections describe how you can review the analysis results:
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.
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.
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
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
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
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
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).
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
The harness model contains the following items:
Signal Builder block
Inputs — A group of signals that falsify
Test Unit — A copy of your model.
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 the harness model to observe the counterexample that falsifies the proof objective in your 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.
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.
|Highlighted Results on the Model|
Generate a detailed analysis report.
|Simulink Design Verifier Reports|
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.
|Simulink Design Verifier Harness Models|
View the data file.
|Simulink Design Verifier Data Files|
View the log file.
|Simulink Design Verifier Log Files|
After you close your model, you can no longer view the analysis results.
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
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
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
Click Apply and then OK to apply your changes and close the Proof Assumption block parameter dialog box.
and keep it open.
Analyze the model that you modified to see how the Proof Assumption block affects the property-proving analysis.
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 the results of the second analysis:
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 the analysis results in the detailed report:
Click Generate detailed analysis report.
In the Table of Contents, click
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,
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.
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.
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.
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.