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:

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:

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 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.