Use a Requirements Table Block to Create Formal Requirements

Since R2022a

Use the Requirements Table block to model formal requirements. You establish formal requirements by using Boolean formulas that check whether the required model behavior occurs during simulation. When you create a requirement in a Requirements Table block, you also create an equivalent requirement in the Requirements Editor. See Configure Properties of Formal Requirements.

Define Formal Requirements

Formal requirements are a set of unambiguous specifications that you express mathematically and execute through simulation. Each formal requirement executes if at least one condition is true for a specified duration. When the requirement executes, the block verifies specified simulation behavior and produces additional simulation data.

To define formal requirements, add a Requirements Table block to your model.

Opening a new Requirements Table block displays a blank requirement. By default, the block opens on the Requirements tab. Each row of the table represents a requirement. The columns specify information used to evaluate each requirement. The columns are:

• Index — A unique identifier for each requirement. This column is read-only.

• Summary — A text-based summary of the requirement. Entries in this column do not affect the block behavior. This column is optional.

• Precondition — A Boolean expression that must be true for a specified duration before evaluating the rest of the requirement.

• Duration — The time, in seconds, during which the precondition must be true before evaluating the rest of the requirement. This column is optional. If left blank, the requirement does not have a duration. You must specify a precondition to use this column. See Using the Duration Column.

• Postcondition — A Boolean expression that must be true if the associated precondition is true for the specified duration. If you do not include a precondition, the block checks the postcondition at each time step.

• Action — An action performed by the block if the associated precondition is true for the specified duration. You can use actions to define a block output or call a function. If you do not include a precondition, the block executes the action at each time step.

You can create multiple requirements, preconditions, postconditions, and actions. To manage columns and requirements, use options available in the Table tab. You can also access additional options with the context menu by right-clicking the requirement index or column header cell.

You can also specify assumptions that define physical constraints of the system in the Assumptions tab. See Add Assumptions to Requirements.

Create Expressions for Formal Requirements

You define preconditions, postconditions, and actions with expressions. Use Boolean expressions for preconditions and postconditions, and use a single equal sign = to define actions. The expressions in each precondition and postcondition cell must evaluate to a scalar logical.

Use data in your expressions to manage information, such as signal values, workspace variables, or constant values. Expressions can also include numerical values and functions. For example, the precondition u >= 0 checks if the data u is greater than or equal to 0, and the action y = 0 sets the data y equal to 0.

You can define preconditions, postconditions, and actions by explicitly listing each full expression in the requirement cells or by listing the left-hand side of the expression in the column header and defining the right-hand side of the expression in the requirement. To write Boolean expressions that use headers in Precondition and Postcondition columns, use the Boolean relational operator of interest, leave the left side blank, and enter the value of interest. To write actions that use headers, enter the value of the action into the cell.

For example, in this table the first postcondition specifies the data y1 in the header, the second specifies y2 in the requirement cell, and the action sets y3 equal to a vector of values.

You can also check if a scalar header equals a single value, multiple values, or a range of values in the Precondition and Postcondition columns. Use these syntaxes to specify the checked values:

Syntax	Description
value	Checks if the header data equals value.
value1,value2,value3,...,valueN	Checks if the header data equals one of the comma-separated values.
[value1,value2]	Checks if the header data is greater than or equal to value1 and is less than or equal to value2.
(value1,value2)	Checks if the header data is greater than value1 and is less than value2.
[value1,value2)	Checks if the header data is greater than or equal to value1 and is less than value2.
(value1,value2]	Checks if the header data is greater than value1 and is less than or equal to value2.

In this table, the precondition checks if u is equal to 1, 2, or 3. The postcondition evaluates the data y1 and y2 by using the same Boolean expression but with different notation. The first postcondition uses header data with interval notation and the second postcondition uses explicit Boolean operators without header data.

To evaluate header data against multiple intervals, combine them with the logical OR operator. For example, [0.3, 0.5] || (0.1, 0.2) is valid. In addition to real numbers, you can also use Inf in an interval to evaluate a bound that goes to infinity. Intervals including Inf must be preceded or followed by a parenthesis. Intervals including Inf can be simplified if the cell contains only one interval. For example, (0.3, Inf) is equivalent to > 0.3.

To specify that the header data should not equal an expression, use the logical NOT operator by entering ~= or ~ to the left of the cell values. You can apply this operator to single values, comma-separated values, or intervals. For example, if you did not want the header data u to fall within the interval [0.3, 0.5], enter ~[0.3, 0.5] or ~=[0.3, 0.5]. For comma-separated values, use only ~.

If your requirement cells contain a lot of content, the cell size can obstruct the expression. To view all of the content, you can adjust the size of the cell or add a new line. To add a new line, finish the first line with ... and then press Alt+Enter.

Use the X Placeholder

When you enter expressions in a header, do not reuse the header expression in the cells of that column. For example, if a header contains the data u, do not enter the expression u >= 0.5 && u <= 0.3 in an associated column cell. Instead, use X as a placeholder for the header. For example, the expression X >= 0.5 && X <= 0.3 in a precondition with u in the header is equivalent to u >= 0.5 && u <= 0.3 without u in the header.

Using the X placeholder can improve readability when the header is long.

Check Array Data in Preconditions and Postconditions

If you use array data in preconditions and postconditions, the block checks if each element of the data satisfies the logical expression and produces a logical array. To check if a precondition or postcondition satisfies an array of values, use functions that evaluate to a scalar logical, such as the isequal or all functions. For example, if y1 is a 1-by-4 array, and you want to check that it equals [1 2 3 4], enter isequal(y1,[1 2 3 4]) or all(y1 == [1 2 3 4]) into the cell.

Use Functions in Requirements Table Blocks

You can use functions and operators in Requirements Table blocks in the requirement cells or column headers. Enter data as arguments to the function or operator like you do with variables in MATLAB^®. In this table, the cell u1 + u2 == 2 and the cell below the header u3 + u4 both check if the sum of the two input data equals 2.

The Requirements Table block does not support functions in headers that write to global variables or an internal state. For example, you cannot use the rand function in a header because rand writes to an internal state each time it generates a number.

Define Block Data

In order to use data in the block, you must enter them in your requirements and define them in the Symbols pane. To open the Symbols pane, open a Requirements Table block. In the Modeling tab, in the Design Data section, click Symbols Pane.

In the Symbols pane, the icon in the Type column indicates the scope of your data. You can set the data scope to be Input, Output, Local, Constant, or Parameter. You can also change the name, the initial data value, and the port number. To modify additional properties, right-click the data name and select Inspect to open the Property Inspector. For more information, see Define Data in Requirements Table Blocks.

As you edit your requirements, the Requirements Table block detects undefined data and marks them in the Symbols pane with the Undefined symbol icon . Unresolved data can cause errors during compilation. To resolve data, click the Resolve undefined symbols button .

Observe or Generate Model Behavior

You can use the Requirements Table block to check model requirements by observing the model behavior, or by generating behavior that can be compared to the model behavior.

Observe Model Behavior

You can use the Requirements Table block to observe the model behavior without executing actions. If the model behavior does not satisfy a precondition, the block does not check the associated postcondition. If the model behavior does not satisfy the postcondition for a requirement when the precondition is satisfied, the Requirements Table block produces a warning in the Diagnostic Viewer. To use the Requirements Table block to observe requirements, use the preconditions to specify model input behavior, and use the postconditions to specify model output behavior. To differentiate between the model inputs and outputs, enable the Treat as design model output for analysis property in the Property Inspector for the data specified in the postconditions. See Treat as design model output for analysis.

This model contains a Requirements Table block that tests a basic subsystem that has two inputs and outputs two values. The Requirements Table block checks whether the inputs and outputs of the subsystem meet the specified requirements by using logical definitions for the preconditions and postconditions.

Open the Requirements Table block to see the requirements specified for the inputs and outputs of the subsystem. The requirements specify logical constraints on the subsystem outputs for each subsystem input. The Requirements Table block captures the subsystem inputs with the data u1 and u2, and captures the subsystem outputs with the data y1 and y2. The block defines the data as input data, which allows the block to capture the subsystem signals as block inputs.

When you run the model, the Requirements Table block checks if the Subsystem block inputs satisfy the preconditions. If the preconditions are met, the Requirements Table block checks if the Subsystem block outputs satisfy the postconditions.

This example Subsystem block satisfies the preconditions and postconditions. To generate a warning, set the postcondition of the first requirement to y1 < 0 and run the simulation again. The Diagnostic Viewer displays a warning message.

Generate Model Behavior

You can also use the Requirements Table block to execute actions when the model meets corresponding preconditions. You specify the action for each requirement by using the Action column.

This model contains a Requirements Table block that tests a subsystem that takes two inputs and creates two outputs. The Requirements Table block takes the subsystem inputs and outputs a set of values if the preconditions are met. Each Requirements Table block output corresponds to one of the outputs from the subsystem. If the output of the subsystem does not equal the corresponding output signal from the Requirements Table block, the Assertion blocks stop the simulation and produce an error.

Open the Requirements Table block to see the two requirements specified for the inputs of the subsystem. The requirements specify logical constraints on the inputs. The block defines the data u1 and u2 as input data, which allows the block to capture the subsystem inputs as block inputs. The block defines the data y1 and y2 as output data.

When you run the model, the Requirements Table block checks whether the Subsystem block inputs meets the preconditions, and assigns the output signals to the values specified in the Action column. The model then compares the outputs from the Subsystem block with the output signals from the Requirements Table block. In this example, the outputs are equal and the assertions pass.