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
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.
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.
sldvdemo_sbr_verification model contains
a property that is falsified, because a constraint is disabled. In
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 the
KEYinput 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
Prove the Properties of the Design Model
to prove the properties:
sldvdemo_sbr_verificationmodel 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
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
KEYinput 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
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
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:
sldvdemo_sbr_verificationmodel, click Open Fixed Model.
sldvdemo_sbr_verification_fixedverification model opens.
Open the Input Constraints subsystem.
This third constraint is now enabled so that
KEYhas an initial value of 0 and changes in increments of 1.
Close the Input Constraints subsystem.
sldvdemo_sbr_verification_fixedmodel, to start the analysis, double-click the Run block.
The analysis proves the validity of the property.