Prove System-Level Properties Using Verification Model
When to Use a Verification Model for Property Proving
If your model has system-wide properties that affect the behavior of the model, you might want to prove the properties without changing the design model. To do this, you create a verification model that includes:
Model block that references the design model
One or more verification subsystems that define the properties and any required constraints
About This Example
The design model sldvdemo_sbr_design
models
the logic for a seat belt reminder light. If the ignition is turned
on, the seat belts are unfastened, and the car exceeds a certain speed,
the seat belt reminder light turns on.
The sldvdemo_sbr_verification
model is a
verification model that defines some constraints and verifies the
properties in the sldvdemo_sbr_design
model. The Model block
in the verification model references the design model, so that the
verification logic exists only in the verification model.
The sldvdemo_sbr_verification
model contains
a property that is falsified, because a constraint is disabled. In
the sldvdemo_sbl_verification_fixed
model, the
constraint is enabled and all the
properties are proven valid.
Understand the Verification Model
Take these steps to understand how the verification model works:
Open the verification model:
The Design Model block is a Model block that references
sldvdemo_sbr_design
. The SBR Stateflow® chart in the design model assumes that theKEY
input is initially 0.Open the Safety Properties subsystem that specifies the properties of the design model that you want to prove.
This subsystem contains a MATLAB Function block called MATLAB Property. The code in this block specifies the property that the seat belt reminder should be on when the ignition is on, the seat belt is not fastened, and the speed is less than 15:
Close the Safety Properties subsystem.
Open the Input Constraints subsystem.
This subsystem defines the following constraints:
The key can have three positions: 0, 1, 2
The speed is constrained to fall between 10 and 30.
The key must start at 0 and can only change by one increment at a time. For example, the key can change from 0 to 1 or 1 to 2, but not from 0 to 2. In this verification model, this constraint is not enabled.
Close the Input Constraints subsystem, but keep the
sldvdemo_sbr_verification
model open.
Prove the Properties of the Design Model
Analyze the sldvdemo_sbr_verification
model
to prove the properties:
In the
sldvdemo_sbr_verification
model window, to start the analysis, double-click the Run button to start the analysis.When the analysis completes, the Simulink® Design Verifier™ log window indicates that one objective is falsified - needs simulation. For more information, see Objectives Falsified - Needs Simulation.
To see which objective was falsified, click Highlight analysis results on model.
The Safety Properties subsystem is highlighted in orange.
Open the Safety Properties subsystem and click the MATLAB Property block.
The Simulink Design Verifier Results window indicates that the statement
sldv.prove(implies(activeCond,SeatBeltIcon))
was false during at least one time step.
Click View counterexample to see the signal values that violated this property.
The Signal Builder block opens with the counterexample. The
KEY
input was initially 2, which is invalid.
To validate the property specified in the Safety Properties
subsystem, you have to make sure that the initial value of KEY
is
0.
Fix the Verification Model
The Input Constraints subsystem in the verification model contained three constraints. The
third constraint, which requires that the initial value of KEY
be
0, and that KEY
can only change in increments of 1, is disabled.
To see how this property is validated when you enable the third constraint:
In the
sldvdemo_sbr_verification
model, click Open Fixed Model.The
sldvdemo_sbr_verification_fixed
verification model opens.Open the Input Constraints subsystem.
This third constraint is now enabled so that
KEY
has an initial value of 0 and changes in increments of 1.Close the Input Constraints subsystem.
In the
sldvdemo_sbr_verification_fixed
model, to start the analysis, double-click the Run block.The analysis proves the validity of the property.