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. 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
0, and the action
y = 0 sets the data
y equal to
You can define preconditions, postconditions, and actions by explicitly listing data in each expression or by listing data in the column header and defining expressions that use the header data. To write Boolean expressions that use header data 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 header data, enter the value of the action directly into the cell.
For example, in this table the first postcondition specifies
y1 in the
header, the second specifies
y2 in the requirement cell, and the action
y3 equal to a vector of values.
You can also check if the header data 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 either 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
When you use header data, do not use the header data 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 the associated column cell.
X as a placeholder for the header data. For example, the
X <= 0.5 && X >= 0.3 in a precondition or
u in the header is equivalent to
u <= 0.5
&& u >= 0.3 without
u in the header. This format can
improve readability when the header is long.
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 meets the preconditions. If the subsystem behavior meets the requirements, the Requirements Table block checks if the Subsystem block outputs satisfy the postconditions. If the model satisfies both postconditions for all of the requirements, the simulation runs without warnings.
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.
Troubleshoot Incomplete and Inconsistent Requirement Sets and Read-Before-Write Errors
Formal requirements must uniquely define the data used in the preconditions, postconditions, and actions at each simulation time step. Three scenarios can violate this principle:
If the block can execute a scenario where at least one data is not defined, the requirement set is incomplete.
If at least one data defined in the requirement set can equal more than one value during simulation, the requirement set is inconsistent.
If you define requirements that use data before the data is written, the requirement set can cause a read-before-write error.
Typically, these scenarios generate an error during simulation, but they can be difficult to detect manually. If you have Simulink® Design Verifier™, you can detect the causes of the scenarios. To analyze the requirements, open the Requirements Table block. In the Table tab, in the Analyze section, click Analyze Table. For more information, see Troubleshoot Requirements Table Blocks.