Requirements Modeling

Model and verify design requirements using property proving

Blocks

Proof Assumption	Constrain signal values when proving model properties
Proof Objective	Define objectives that signals must satisfy when proving model properties
Assertion	Check whether signal is zero
Detector	Detect true duration on input and construct output true duration based on output type
Extender	Extend true duration of input
Implies	Specify condition that produces a certain response
Within Implies	Verify response occurs within desired duration
Verification Subsystem	Specify proof or test objectives without impacting simulation results or generated code

Functions

`sldv.assume`	Proof assumption function for Stateflow charts and MATLAB Function blocks
`sldv.prove`	Proof objective function for Stateflow charts and MATLAB Function blocks
`sldvextract`	Extract subsystem or subchart contents into new model for analysis
`sldvoptions`	Create design verification options object
`sldvrun`	Analyze model
`sldvreport`	Generate Simulink Design Verifier report

Topics

What Is Property Proving?
Brief overview of proving properties.
Workflow for Proving Model Properties
Outlines a process for proving properties of your model.
Prove Properties in a Model
Provides an example that walks you through the process of proving model properties.
Prove System-Level Properties Using Verification Model
An example that uses a verification model to prove system-level properties.
Prove Properties in a Subsystem
Explains how to prove properties in a subsystem.
Debug Property Proving Violations by Using Model Slicer
Debug property proving violations using Model Slicer
Design and Verify Properties in a Model
You can use Simulink® Design Verifier™ to model design requirements as properties and then prove properties in a model.
Parameter Configuration for Analysis
Overview of parameter configuration for Simulink^® Design Verifier™ analysis.
Model Requirements
The Simulink Design Verifier block library includes a sublibrary Example Properties.
Use Parameter Table
An example of how to specify parameters as variables for analysis.
Specify Parameter Configuration for Full Coverage
An example of how to specify parameter constraint values to achieve full model coverage.
Design Verifier Pane: Property Proving
Specify options that control how Simulink Design Verifier proves properties for the models it analyzes.
Design Verifier Pane: Parameters and Variants
Specify options that control how Simulink Design Verifier uses parameter configurations when analyzing models.
Review Analysis Results
Review analysis results in the Simulink Design Verifier Results Summary window.
What is a Specification Model?
Overview of specification model and its use in requirements-based verification.
Isolate Verification Logic with Observers
Describes the observer support for simulink design verifier.

Featured Examples

Property Proving Using MATLAB Function Block

Verify the seat belt reminder design model. The Safety Properties block below it contains a property specified in MATLAB that indicates when the icon should be active. Simulink Design Verifier analyzes the design model and safety property to prove correctness or to identify counterexamples. In this model, the property is violated because the design implicitly assumes that the KEY input starts at 0 and changes by increments of 1.

Open Example

Property Proving Using MATLAB Truth Table Block

Verify the seat belt reminder design model referenced in the top block above. The Safety Properties block below it contains a property specified in MATLAB Truth Table that indicates when the SeatBeltIcon output should be active. Simulink Design Verifier analyzes the design model and safety property to prove correctness or to identify counterexamples. In this model, the property is proven under the explicit assumption that the KEY input starts at 0 and changes by increments of 1.

Open Example

Property Proving with an Assumption Block

Perform a Simulink Design Verifier property proof using a Proof Assumption block. It attempts to prove that when the sum of the current and six previous input values is greater than 6, the output equals 2. The model includes a Proof Assumption block that constrains the input to be 0 or 1. Simulink Design Verifier searches for violations of 20 or fewer time steps. It is unable to find a violation because the property is valid under the assumption.

Open Example

Property Proving with an Invalid Property

Find an invalid property using Simulink Design Verifier property proving analysis. It attempts to prove that when the sum of the current and six previous input values is greater than 6, the output equals 2. In this case, the property is invalid because a single large input value (e.g. 255) causes the sum to be greater than 6. Simulink Design Verifier produces a counterexample that demonstrates the violation.

Open Example

Use Observer Reference Blocks for Property Proving Analysis

Perform property proving analysis using Observer Reference blocks.

Open Script