Identify Inconsistent and Incomplete Formal Requirement Sets

Since R2022a

When using a Requirements Table block, you can identify inconsistent and incomplete requirement sets, and find read-before-write errors. These problems can depend on semantic errors in individual requirements or can be caused by issues in the requirement set.

Analyze the Block

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 assigned a value, 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.

Inconsistency Issues

Inconsistency issues occur when the block can perform different behaviors for a single combination of input values. For example, the table below illustrates inconsistent requirements. When analyzed, it finds two inconsistency issues, which are highlighted red and include an alert icon .

The Analysis Results pane displays additional details on the inconsistency issues.

Incompleteness Issues

Requirements have incompleteness issues when the block does not comprehensively specify outputs for possible input values. For example, in the model used in the Generate Model Behavior example, the table includes two incompleteness issues.

You can fix these issues by introducing requirements that define when u1 and u2 are less than or equal to 0, or by creating an assumption that constrains u1 and u2 to be greater than or equal to 0. For more information about how to write assumptions, see Add Assumptions to Requirements.

Read-Before-Write Issues

Read-before-write issues occur when a requirement attempts to read data that has not yet been defined. In most cases, you can minimize the potential for read-before-write issues by not calling output data in preconditions and postconditions, or by specifying the requirements in order. For more information, see Establish Hierarchy in Requirements Table Blocks. For example, in this table, the first requirement reads the output data y2 before y2 has an assigned value.

When you analyze the requirements, the block detects a read-before-write issue.

You can create requirement preconditions that rely on output data if you list the requirements in order and enable the Enable outputs in preconditions property in the block. See Enable outputs in preconditions. For example, the model used in Example Using Requirement Order does not produce requirement issues because the requirement order specifies the local data before the other requirements need it. If you change the order of the requirements so that Requirements 3 and 4 are listed first, then analyze the requirements, the analysis finds two read-before-write issues.

Note

If you write more than two requirements that read the same data before the data is written, the analysis detects the issue in only the first listed requirement with the issue. After resolving the issue, rerun the analysis to detect the next read-before-write issue.

Include the Entire Model in Analysis

By default, the Requirements Table block assumes that input data is independently generated. If the input data is not independent, you may find that you must over specify your requirements to prevent issues. You can prevent this problem by doing the following:

• Configure the block to identify the source of the data in the context of the entire model. In the Table tab, in the Analyze section, expand the Analyze Table menu and enable Include entire model.

• Specify assumptions based on how physical or mathematical limitations prevent data from being certain values. See Add Assumptions to Requirements.

Analyze Rigid and Flexible Requirements

Depending on how you define the relationships between data, you can establish two kinds of requirements: rigid and flexible. In addition to individual requirements, sets of requirements in the block can also be rigid or flexible.

Rigid Requirements

If a requirement postcondition specifies an exact value, or if the requirement specifies only an action, the requirement is rigid. You express these requirement postconditions with the double equals sign ==. For example, a requirement with a postcondition y == 0 is rigid. If each requirement in the requirement set is rigid, then the requirement set is rigid.

Flexible Requirements

If a requirement postcondition can satisfy a range of values, then the requirement is flexible. For example, a requirement with a postcondition y >= 0 or y >= 0 && y < -2 is flexible. Additionally, postconditions that specify multiple values also create flexible requirements. For example, a requirement with a postcondition u == 3 || u == 4 is flexible. If at least one requirement in the requirement set is flexible, then the entire requirement set is flexible.

Analysis Limitations

You can analyze the Requirements Table block with some features only if the requirement set is rigid. These features include:

• Persistent variables.

• Using arrays as Requirements Table block outputs, or inputs with the Treat as design model output for analysis property enabled.

• Some functions. Incompatible functions will cause an error when analyzing the table. The error message identifies the responsible function.