What Is Property Proving?
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 requirement on the model that involves a number of input and output signals modeled as a logical expression that needs to be proved.
The Simulink Design Verifier™ software performs a formal analysis of your model to prove or disprove the specified properties. After completing the analysis, the software offers several ways for you to review the results:
Highlighted on the model
A harness model with test cases
A detailed HTML report
The Simulink Design Verifier software provides two blocks so you can specify property proofs in your Simulink models:
Proof Objective — Define the values of a signal to prove
Proof Assumption — Constrain the values of a signal during a proof
Blocks from the Model Verification library in the Simulink software behave like Proof Objective blocks during Simulink Design Verifier proofs. You can use Assertion blocks and other Model Verification blocks to specify properties of your model. For more information about these blocks, see Model Verification.
The Simulink Design Verifier software provides two Stateflow and MATLAB® for code generation functions to specify property proving for a Simulink model or Stateflow chart:
sldv.prove— Specifies a proof objective
sldv.assume— Specifies a proof assumption
Identify mathematical relationships for proving properties in a form that can be more natural than using block parameters
Support specifying multiple objectives, assumptions, or conditions without complicating the model.
Provide access to the power of MATLAB.
Support separation of verification and model design.
For an example of how to use these proof functions, see the
sldv.prove reference page.
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.