指定并验证设计需求

根据需求验证设计，使用输入假设优化反例

安全需求定义模型中的意外行为。Simulink^® Design Verifier™ 使用属性证明来验证与模型需求相关联的属性在所有可能的输入值下是否成立，或者提供导致违规的反例。您可以使用 Simulink Design Verifier 将设计需求建模为属性，然后Prove Properties in a Model。

模块

全部展开

验证设计需求

Proof Assumption	Constrain signal values when proving model properties
Proof Objective	Define objectives that signals must satisfy when proving model properties
Assertion	检查信号是否为零
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

函数

全部展开

验证设计需求

`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

主题

入门知识

Workflow for Proving Model Properties
Outlines a process for proving properties of your model.
What Is Property Proving?
Brief overview of proving properties.
Prove Properties in a Model
Provides an example that walks you through the process of proving model properties.
Use Parameter Table
An example of how to specify parameters as variables for analysis.
指定信号范围
指定信号在仿真期间可以达到的最小值和最大值。通过指定信号在仿真过程中可以达到的最小值和最大值，充分指定您的设计并优化数据类型和生成的代码。
Minimum and Maximum Input Constraints
An overview of how the Simulink Design Verifier analysis considers specified input minimum and maximum values.
Specify Input Ranges on Simulink and Stateflow Elements
Describes how the analysis handles minimum and maximum values on Simulink and Stateflow^® elements.

用于验证和确认的需求建模

What Is a Specification Model?
Overview of specification model and its use in requirements-based verification. (自 R2022b 起)
Model Requirements
The Simulink Design Verifier block library includes a sublibrary Example Properties.
Isolate Verification Logic with Observers
Describes the observer support for Simulink Design Verifier.
Using Specified Input Minimum and Maximum Values as Constraints
This example shows how to use input port minimum and maximum values as analysis constraints by Simulink® Design Verifier™ during both test generation and property proving.
Use Specification Models for Requirements-Based Testing
Follow a systematic approach to verify your design model against requirements. (自 R2022b 起)

通过属性证明进行验证

Prove Properties in a Model
Provides an example that walks you through the process of proving model properties.
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.
Debug Property Proving Violations by Using Model Slicer
Use Model Slicer to debug your design with assertion blocks.
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.
Check for Specified Minimum and Maximum Value Violations
Describes how to analyze the model to verify that specified design minimum and maximum values are honored.
Specification of Input Ranges in sldvData Fields
Describes the sldvData fields for minimum and maximum input values.
Property Proving Using MATLAB Function Block
This example shows how to verify the seat belt reminder design model.
Property Proving Using MATLAB Truth Table Block
This example shows how to verify the seat belt reminder design model referenced in the top block above.
Property Proving with an Assumption Block
This example shows how to perform a Simulink® Design Verifier™ property proof using a Proof Assumption block.
Property Proving with an Invalid Property
This example shows how to find an invalid property using Simulink® Design Verifier™ property proving analysis.
Prove Properties in Large Models
Describes workflows and best practices for proving properties in large models.

精选示例

Validate Requirements by Analyzing Model Properties

Analyze a control system model for adherence to requirements modeled as properties, and investigate property violations by using dependency analysis.

打开模型

Property Proving Workflow for Cruise Control

Find a property violation by using Simulink® Design Verifier™ property proving analysis. You model safety requirements as properties and then verify the design model against requirements.

打开脚本

Property Proving Workflow for Thrust Reverser

Verify safety properties in a thrust reverser design model. The Properties block below it contains four safety properties. Simulink® Design Verifier™ analyzes the design model and safety properties to prove correctness or to identify counterexamples. The use of model referencing eliminates the need to add verification content to the design model, allowing the verification content to exist independently from the design.

打开脚本

Property Proving with Multiple Properties

Perform a property proving analysis with multiple properties. The model is configured for the analysis to attempt to prove that:

打开脚本

Property Proving Workflow for Fixed-Point Cruise Control with Block Replacements

Prove properties in a fixed-point cruise control algorithm. It references the design model using model reference so that the original design model is unchanged. A block replacement rule specifies the property that checks if an overflow is possible. The verification subsystem specifies an assumption on the range of the speed input during property proving. This model configures Simulink Design Verifier to apply a block replacement to the Sum block that feeds the outport of the fixed-point PI Controller in the referenced model and return a counterexample that demonstrates an overflow.

打开脚本