Main Content

Design and Verify Properties in a Model

Open Script

You can use Simulink® Design Verifier™ to model design requirements as properties and then prove properties in a model. To verify that the properties associated with the model requirements hold under all possible input values, use property proving analysis. If the requirement fails, Simulink Design Verifier provides counterexamples to debug the failure.

This example explains how you can model design requirements as properties by using a Proof Objective block and then verify the property for simplified cruise control model discussed in Analyze a Simple Cruise Control Model.

Step 1: Design Property Using Verification Subsystem

The model sldvexSimpleCruiseControlProperties consists of Verification Subsystem, that consists of function requirements modeled by using Proof Objective block.

load_system('sldvexSimpleCruiseControlProperty');
open_system('sldvexSimpleCruiseControlProperty/Verification Subsystem');

Step 2: Perform Property Proving Analysis

On the Apps tab, click arrow on the far right of the Apps section. Under Model Verification, Validation, and Test gallery, click Design Verifier.

To perform property proving analysis, click Prove Properties. The software analyzes the model and displays the results in the Results Summary window. The result indicates that one objective is valid under approximation.

Step 3: Review Analysis Results

On the Design Verifier tab, in the Review Results section, click Highlight in Model.

The property that is valid under approximation is highlighted in orange. Click the Proof Objective block. The Results Inspector window displays the objectives of the Proof Objective block.

To view the HTML report, in the Review Results section, click HTML Report. The Proof Objective Status chapter lists the proof objective that is found valid under approximation.

See also