Main Content

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.

Isolate Verification Logic with Observers

Describes the observer support for simulink design verifier.

Featured Examples