Requirements Modeling

Model and verify design requirements using property proving

Blocks

Proof AssumptionConstrain signal values when proving model properties
Proof ObjectiveDefine objectives that signals must satisfy when proving model properties
AssertionCheck whether signal is zero
DetectorDetect true duration on input and construct output true duration based on output type
ExtenderExtend true duration of input
ImpliesSpecify condition that produces a certain response
Within ImpliesVerify response occurs within desired duration
Verification SubsystemSpecify proof or test objectives without impacting simulation results or generated code

Functions

sldv.assumeProof assumption function for Stateflow charts and MATLAB Function blocks
sldv.proveProof objective function for Stateflow charts and MATLAB Function blocks
sldvextractExtract subsystem or subchart contents into new model for analysis
sldvoptionsCreate design verification options object
sldvrunAnalyze model
sldvreportGenerate 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 Constraint Values

Overview of parameter configuration for Simulink® Design Verifier™ analysis.

Model Requirements

The Simulink Design Verifier block library includes a sublibrary Example Properties.

Define Constraint Values for Parameters

An example of how to specify parameters as variables for analysis.

Specify Parameter Constraint Values 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

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.

Featured Examples

Property Proving Using MATLAB Function Block

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

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

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

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

Simulink Design Verifier Documentation

Support