Especificar y verificar requisitos de diseño
Los requisitos de seguridad definen comportamientos no deseados en un modelo. Simulink® Design Verifier™ utiliza demostración de propiedades para comprobar que las propiedades asociadas a los requisitos del modelo se mantienen con todos los valores de entrada posibles o proporciona contraejemplos que generan infracciones. Puede utilizar Simulink Design Verifier para modelar requisitos de diseño como propiedades y, luego, Prove Properties in a Model.
Bloques
Funciones
Temas
Comenzar aquí
- Prove Model Properties
Workflow and techniques for proving model properties. - Prove Properties in a Model
Prove model properties that you specify using a Proof Objective block. - Use Parameter Table to Find Constraints
An example of how to specify parameters as variables for analysis. - Specify Signal Ranges
Specify the minimum and maximum value that a signal can attain during simulation. Fully specify your design and optimize data types and the generated code by specifying the minimum and maximum value that a signal can attain during simulation. - 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. - Verify and Validate a Model and Code
Define requirements, test models and code, check for design errors and standards compliance, and measure test coverage.
Modelado de requisitos para verificación y validación
- Specify Input Ranges on Simulink and Stateflow Elements
Describes how the analysis handles minimum and maximum values on Simulink and Stateflow elements. - Use Specification Models for Requirements-Based Testing
Follow a systematic approach to verify your design model against requirements. (Desde R2022b)
Verificación mediante demostración de propiedades
- Prove Properties in a Model
Prove model properties that you specify using a Proof Objective block. - Property Proving Using Proof Objective Block
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. - 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. - 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
Use Simulink Design Verifier workflows and best practices for proving properties in large models.
Ejemplos destacados
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.
Find and Debug Property Violation Using Simulink Design Verifier
Use Simulink Design Verifier to find and debug property violation in model.
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.
Use Observer Reference Blocks for Property Proving Analysis
Perform property proving analysis using Observer Reference blocks.
Prove Properties with Requirements Table Blocks
Use a Requirements Table block and Simulink Design Verifier to prove properties of a model.
