Main Content

Leverage Evaluation Order of Formal Requirements

Since R2022a

The Requirements Table block evaluates requirements by starting at the first requirement and working downward. You can leverage this behavior by assigning values to data and then using the data in requirements listed later in the requirement set.

For example, if you want to reference local data in the preconditions of other requirements:

  1. List the requirements that define the local data values first in the set.

  2. List the requirements that require the local data in preconditions later.

  3. Verify that your requirements do not read data before being written.

    • If you have Simulink® Design Verifier™, you can analyze the requirements to detect instances where data is read before it is written. In the Table tab, in the Analyze section, click Analyze Table. See Detect Read-Before-Write Issues.

For more information on how to define requirements, see Use a Requirements Table Block to Create Formal Requirements.

You can reference output data in preconditions if the Enable outputs in preconditions property is enabled or if the data is an argument in the getPrevious operator. To enable this property, open the Requirements Table block. In the Modeling tab, in the Design Data section, click Property Inspector. In the Properties tab, enable the Enable outputs in preconditions property. See Enable outputs in preconditions.

Example Using Requirement Order

This example shows how requirement order affects data in Requirements Table blocks.

Examine the Requirements

Open the Requirements Table block. The block uses the input data sensorv and sensor to determine the value of the local data value. The requirements then use value to determine the value of the output data output.

If you define Requirements 3 and 4 before Requirements 1 and 2, the requirements do not define value before value is needed, which causes a read-before-write error during simulation.

See Also

Related Topics