Prove Model Properties

A property is a requirement that you model in Simulink^® or Stateflow^® or by using MATLAB Function or Requirements Table blocks. A property can be a simple requirement, such as a signal in your model that must attain a particular value or range of values during simulation. A property can also be a more complex requirement, such as a number of input and output signals that must evaluate to a logical expression. The Simulink Design Verifier™ software performs a formal analysis of your model to prove or disprove these properties and offers various ways for you to review the results:

Highlighted on the model
A detailed HTML report
A harness model with counterexamples

Workflow for Proving Model Properties

To prove properties of your design model, use the following workflow:

Determine the objectives for verifying the design of your model.
1. Check your requirements for consistency and completeness.
2. Decide whether you want to instrument the model itself or separate the property specification by using techniques such as a verification subsystem or verification model.
3. Define the properties to prove as proof objectives.
4. Define analysis constraints by specifying assumptions that apply to the proof objectives.
Analyze the model to prove the properties.
1. Check the compatibility of your model with Simulink Design Verifier property proving.
2. Specify options that control how Simulink Design Verifier proves the properties of your model.
3. Run property proving analysis and review the results.
If the results show disproved properties, debug the violations. Fix the failures and then re-analyze the model.

Define Proof Objectives and Assumptions

Decide How to Instrument the Model

To define properties for Simulink Design Verifier to prove, you must connect proof objectives to the associated signals in the model. The best practice is to separate the proof objective logic from the model by using the methods in the following table. Alternatively, you can instrument the model itself by connecting proof objectives directly to the model.

Method	Purpose	More Information
Observer Reference block	Separate your properties and associated logic from your design model by inserting an observer reference into your design model. Associate the reference with a separate observer model that contains the property specifications, such as a verification subsystem.	Use Observer Reference Blocks for Property Proving Analysis Isolate Verification Logic with Observers
Verification model	Organize system-level properties in a top-level model. This top model references the design model that you want to verify by using a Model block. The verification model also contains one or more verification subsystems that define the system-wide properties to prove and constraints on those properties.	Prove System-Level Properties Using Verification Model
Verification Subsystem block	Inside the subsystem, you add other blocks or elements to represent the specific individual requirements. This block lets you add logic to the model for the purpose of Simulink Design Verifier property proving without affecting code generation.	Verification Subsystem

Define Proof Objectives

Define your proof objectives by using the methods in the following table. You can organize these objectives and separate them from the model design logic by using the methods in the previous section.

Method	Purpose	More Information
Proof Objective block	Define objectives that signals must satisfy. This block does not affect simulation or generated code.	Proof Objective
Model Verification library blocks (Simulink)	Define objectives that signals must satisfy. These blocks behave like Proof Objective blocks during Simulink Design Verifier property proving. To prevent these blocks from affecting the generated code, put them inside a verification subsystem.	Model Verification
`sldv.prove` function	Define proof objectives in a MATLAB Function block, Truth Table block, or Stateflow chart. The function enables you to: Specify mathematical relationships for proving properties in a form that can be more natural than using block parameters. Specify multiple objectives, assumptions, or conditions without complicating the model. Separate verification from the model design.	`sldv.prove`
`verify` statements	Define proof objectives in a Test Sequence block, Test Assessment block, or Stateflow chart. These statements enable you to: Specify mathematical relationships for proving properties in a form that can be more natural than using block parameters. Specify multiple objectives, assumptions, or conditions without complicating the model. Separate verification from the model design.	`verify` (Simulink Test)
Requirements Table block (Requirements Toolbox)	Define formal requirements to prove. You can input multiple signals into the Requirements Table block and use the block to define multiple formal requirements that property proving analysis can verify. A formal requirement includes: A precondition that simulation data must satisfy for analysis to check the postcondition A postcondition that defines the objective behavior for simulation data If you specify model properties by using a Requirements Table block, you can check the requirements for consistency and completeness before proving the properties. For an example, see Analyze Requirements Table Blocks for Requirements Specification Problems (Requirements Toolbox).	Requirements Table (Requirements Toolbox) Prove Properties with Requirements Table Blocks

Note

Simulink Design Verifier blocks and functions are saved with a model. If you open the model on a MATLAB^® installation that does not have a Simulink Design Verifier license, you can see the blocks and functions, but they do not produce results.

Define Analysis Constraints

If your proof objectives should be checked only under certain conditions, you can specify those conditions by defining analysis constraints, or proof assumptions, by using one of the methods in the following table.

Warning

Simulink Design Verifier applies the proof assumptions to all enabled proof objectives. Do not specify assumptions that contradict some aspect of another assumption. Contradictory assumptions can invalidate the entire analysis because they can never be satisfied.

Method	Purpose	More Information
Proof Assumption block	Define analysis constraints that signals must satisfy for proof objectives. This block does not affect simulation or generated code.	Proof Assumption
`sldv.assume` function	Define analysis constraints in a MATLAB Function block, Truth Table block, or Stateflow chart. The function enables you to: Specify mathematical relationships for proving properties in a form that can be more natural than using block parameters. Specify multiple objectives, assumptions, or conditions without complicating the model. Separate verification from the model design.	`sldv.assume`
Parameter configuration	Define a group of constraints on model parameter values to use during analysis.	Create Parameter Configuration for Simulink Design Verifier Analysis
Assumptions in the Requirements Table block (Requirements Toolbox)	Define analysis constraints for formal requirements in a Requirements Table block.	Add Assumptions to Requirements (Requirements Toolbox)

Prove Properties

Check Model Compatibility

To prove model properties, you must make sure the model is compatible with Simulink Design Verifier. Before property analysis, you can check the compatibility of your model. For an example, see Check Compatibility of Example Model. During property analysis, the software automatically performs a compatibility check and reports incompatibilities.

Configure Options for Property Proving

To optionally control how Simulink Design Verifier proves properties of your model, you can set model configuration parameters on the Design Verifier Pane: Property Proving.

Run Model Analysis

Execute the Simulink Design Verifier analysis. You can review the results by using these options:

Highlight the analysis results on the model. See Highlight Results on the Model.
Generate an HTML report that includes detailed results such as analysis time and counterexamples. See Review Results from Analysis Report.
Create a harness model with counterexamples that disprove the objectives. See Use Harness Model for Test Simulations.
Review the results programmatically by using the MAT file that contains Simulink Design Verifier data. See View and Understand Analysis Results from Data Files.

Debug Disproved Properties Using Counterexamples

If the analysis disproves any properties, Simulink Design Verifier generates counterexamples in a harness model. You can use the counterexamples to debug the failure. To see the falsified properties, click Run All in the harness model. Then fix the model and run the counterexample again to verify your fix. When you are satisfied that the model has no more falsified properties, run the complete property proving analysis again.

You can also debug disproved properties by using Model Slicer. Model Slicer debugging:

Adds the falsified property as a starting point
Simulates the model using the counterexample and pauses at the time step of the failure
Highlights blocks and displays port values that lead to the falsified property

After you address the disproved properties, run the model analysis again. For more information, see Find and Debug Property Violation Using Simulink Design Verifier and Debug Property Proving Violations by Using Model Slicer.