Prove Model Properties Using Simulink Design Verifier

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

Proof Blocks to Specify Property Proofs

The Simulink Design Verifier software provides two blocks so you can specify property proofs in your Simulink models:

Proof BlocksDescription
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.

Proof Functions to Specify Property Proving

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:

Proof FunctionsDescription
sldv.prove

Specifies a proof objective

sldv.assume

Specifies a proof assumption

These functions:

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

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.

Workflow for Proving Model Properties

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

  1. Determine the verification objectives for your design model, e.g., based on your requirements specifications.

  2. Instrument your design model to specify proof objectives and proof assumptions.

    • For simple properties, instrument your model with blocks or MATLAB functions that specify the proof objectives.

    • For system-level properties, construct a verification model that contains a Model block that references the design model and define the properties on the design model interface using the same inputs and outputs.

  3. Define analysis constraints using the Proof Assumption block or sldv.assume. These constraints apply to all enabled proof objectives.

    Note

    The proof assumptions are applied to all enabled proof objectives. Make sure that you do not specify any contradictory assumptions because that might invalidate the entire analysis.

  4. Specify options that control how Simulink Design Verifier proves the properties of your model.

  5. Execute the Simulink Design Verifier analysis and review the results.

For an exercise that demonstrates this workflow, see Prove Properties in a Model.

See Also

Topics