Use a Requirements Table Block to Create Formal Requirements
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 duration is
0. 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
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
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:
|Checks if the header data equals |
|Checks if the header data equals one of the comma-separated values.|
|Checks if the header data is greater than or equal to |
|Checks if the header data is greater than |
|Checks if the header data is greater than or equal to |
|Checks if the header data is greater than |
In this table, the precondition checks if
u is equal to
3. The postcondition
evaluates the data
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
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,
Inf) is equivalent to
To specify that the header data should not equal an expression, use the logical
NOT operator by entering
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
fall within the interval
[0.3, 0.5], enter
~=[0.3, 0.5]. For comma-separated values, use
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 the cell by using the Alt+Enter keyboard shortcut.
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,
X >= 0.5 && X <= 0.3 in a precondition with
u in the header is equivalent to
u >= 0.5 && u <=
u in the header.
X placeholder can improve readability when the header is
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
all functions. For example, if
y1 is a 1-by-4 array, and you want to check that it equals
2 3 4], enter
isequal(y1,[1 2 3 4]) or
all(y1 == [1 2 3 4]) into the
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
u3 + u4 both check if the sum of the two input data equals
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.
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
u2, and captures the subsystem outputs with the data
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
u2 as input data, which allows the block to capture the subsystem inputs as block inputs. The block defines the data
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.