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

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.

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.

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

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 a specification model to perform requirements-based testing. In this example, you follow a systematic approach to verify your design model against requirements. For a detailed description of specification model, see What is a Specification Model?.