|
|
|
| R2012a Documentation → Simulink Design Verifier | |
Learn more about Simulink Design Verifier |
|
| Contents | Index |
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 the Simulink Design Verifier software.
In this example, you perform the following tasks.
| Task | Description | See... |
|---|---|---|
| 1 | Construct the example model. | |
| 2 | Verify that your model is compatible with the Simulink Design Verifier software. | |
| 3 | Add a Proof Objective block to your model to prepare for its proof. | |
| 4 | Configure the Simulink Design Verifier software 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 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 the Simulink Design Verifier software 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:
In the model window, select Simulation > Configuration Parameters.
On the left side of the Configuration Parameters dialog box, in the Select tree, click the Solver category. On the right side, under Solver options:
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.
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 the Simulink Design Verifier software before you start the analysis:
Open the ex_property_proving_example_basic model.
In the model window, select Tools > Design Verifier > Check Model 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 the Simulink Design Verifier software 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 Handling Incompatibilities with Automatic Stubbing.
Prepare your example model so that you can prove its properties with the Simulink Design Verifier software. 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 the Simulink Design Verifier software to prove properties of the ex_property_proving_example_basic model that you instrumented:
Open the ex_property_proving_example_basic model.
In your Simulink model window, select Tools > Design Verifier > Options.
On the left side of the Configuration Parameters dialog box, in the Select tree, select the Design Verifier category. Under Analysis options on the right side, set the Mode parameter to Property proving.
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 the Simulink Design Verifier software proves properties of your model. For more information, see Design Verifier Pane: Property Proving. |
Save the ex_property_proving_example_basic model.
To analyze the ex_property_proving_example_basic model, in the model window, select Tools > Design Verifier > Prove Properties. The Simulink Design Verifier software 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 log 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.
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 log 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 the Simulink Design Verifier software identified a counterexample that falsifies an objective in your model.
Scroll back to the top of the browser window. In the Table of Contents, click Proof Objectives Status.
The Objectives Falsified with Counterexamples table lists the proof objectives that the Simulink Design Verifier software 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 the Simulink Design Verifier software 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 ex_property_proving_example_basic_harness.mdl.
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 the harness model to observe the counterexample that falsifies the proof objective in your model:
In the ex_property_proving_example_basic model window, select View > 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.
In your harness model window, select Simulation > Start to begin the simulation.
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.
If you close the analysis results so you review any falsified objectives, you may need to review the analysis results again. As long as your model remains open, you can view the results of your most recent Simulink Design Verifier analysis results in the Model Explorer. After you close your model, you can no longer view any analysis results.
In the model window, select Tools > Design Verifier > Latest Results. The Model Explorer opens, and the results of the latest Simulink Design Verifier analysis appear in the right-hand pane.
For any Simulink Design Verifier analysis, from the Model Explorer, you can perform any of 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. | Harness Model |
View the data file. | Simulink Design Verifier Data Files |
View the log file. | Simulink Design Verifier Log Files |
Modify the simple Simulink model whose proof objective the Simulink Design Verifier software 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, the Simulink Design Verifier software 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.
Analyze the model that you modified to see how the Proof Assumption block affects the property-proving analysis.
In the ex_property_proving_example_basic model window, select Tools > Design Verifier > 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 Summary.
The Summary chapter indicates that the Simulink Design Verifier software 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 the Simulink Design Verifier software 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 the Simulink Design Verifier software 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 states 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.
A thorough proof of your model 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.
Techniques for Proving Properties of Large Models gives detailed information about strategies you can use to improve the performance of a property-proving analysis of a large model.
 | Workflow for Proving Model Properties | Using a Verification Model to Prove System-Level Properties |  |
Learn more about Simulink through this collection of videos, articles, technical literature and the Getting Started with Simulink Guide.
| © 1984-2012- The MathWorks, Inc. - Site Help - Patents - Trademarks - Privacy Policy - Preventing Piracy - RSS |
