Prove Properties with Requirements Table Blocks

Since R2023a

This example shows how to use a Requirements Table block and Simulink® Design Verifier™ to prove the properties of a engine thrust reverser system.

When you use a Requirements Table block and Simulink Design Verifier for property proving:

1. Each requirement in the block defines a formal requirement that you can use to test properties of a model, subsystem, or block. In this example, the Requirements Table block represents the requirements as preconditions and postconditions.

2. Each requirement in the block produces a corresponding requirement in the Requirements Editor. See Configure Properties of Formal Requirements (Requirements Toolbox).

3. Simulink Design Verifier produces proof objectives for the requirements in the requirement set. The postconditions define the logical conditions that you would normally define in Proof Objective blocks. The block evaluates the proof objective associated with a postcondition only if the precondition is true.

For more information, see Use a Requirements Table Block to Create Formal Requirements (Requirements Toolbox) and What Is Property Proving?.

View the Requirements in the Requirements Table Block

Open the example model, property_proving_reqtable. In this example, you test the properties of the engine thrust reverser system, which is modeled by the chart, ThrustReverserDeployLogic. The Requirements Table block uses the chart input signals and deploy output signal to observe the chart behavior. The block defines data in expressions to assess the inputs and outputs of the chart. See Define Data in Requirements Table Blocks (Requirements Toolbox).

To view the verification logic associated with each requirement, open the Requirements Table block. The requirements correspond to the requirements in the requirement set used in the example Validate Requirements by Analyzing Model Properties. The block proves these properties:

1. The thrust reverser shall not deploy if the airspeed is greater than 150 knots.

2. The thrust reverser shall not deploy if the aircraft is in the air, as indicated by the value of the weight on wheels sensors. If the aircraft is in the air, the signal value for each of two weight on wheels (WOW) sensors is false.

3. The thrust reverser shall not deploy if the value of either thrust sensor is positive.

4. The thrust reverser shall not deploy if the rotational speed of the landing gear wheels is less than a threshold value.

Each requirement defines a property. If the preconditions are valid, the postcondition must also be satisfied to prove the property.

Prove Properties

To prove the properties, in the Design Verifier tab, click Prove Properties. In this example, the properties of the chart are proven. The Requirements Table block highlights the postconditions associated with the proven proof objectives in green.

If the requirement proof objective is falsified, the block highlights the requirement in red. Otherwise, if Simulink Design Verifier is unable to prove or disprove the proof objective, the block highlights the requirement in yellow. You can investigate this behavior by replacing the chart in this example with the first iteration of the chart used in the Validate Requirements by Analyzing Model Properties example.