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.

Related Topics

• Property Proving Workflow for Cruise Control
• Property Proving Workflow for Fixed-Point Cruise Control with Block Replacements
• Property Proving Workflow for Thrust Reverser