Identify Inconsistent and Incomplete Formal Requirement Sets

Since R2022a

If you have Simulink^® Design Verifier™, you can identify inconsistent and incomplete requirements sets in the Requirements Table block. A requirement set is incomplete if the block can execute a scenario where at least one data is not assigned a value. A requirement set is inconsistent if at least one data defined in the requirement set can equal more than one value during simulation.

To analyze the requirements for inconsistency and incompleteness issues, open the Requirements Table block. In the Table tab, in the Analyze section, click Analyze Table. For more information on the issues that table analysis detects, see Analyze Requirements Table Blocks for Modeling Problems.

Inconsistency Issues

Inconsistency issues occur when the block can perform different behaviors for a single combination of input values. For example, the table illustrates inconsistent requirements. Table analysis finds two inconsistency issues, which it highlights in red and flags with the alert icon .

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

You can fix inconsistency issues by modifying requirements so that only one behavior is defined for a single combination of input values. In this table, requirements 2.2 and 2.3 both define block outputs for y1 and y2 when u1 is greater than or equal to 0 and u2 is less than 0. To resolve the inconsistency issues, delete requirement 2.2 or 2.3, or redefine the requirement preconditions.

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 incompleteness issues by specifying outputs for all possible input values. For example, you can resolve these incompleteness 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.

Suppress Incompleteness Issues

You can suppress incompleteness issues for an output during simulation or analysis. For example, you may want to suppress incompleteness issues when you have not modeled the entire requirement set, but want to analyze the model for other issues. You may also want to suppress incompleteness issues when certain requirements are not in the design scope and you are not concerned with an output and want to exclude it from incompleteness checks. When you suppress incompleteness issues for a model output and analyze the table, incomplete data is not flagged as incomplete and the Analysis Results pane does not display issues.

To suppress incompleteness issues for an output, use the anyValue function. You can only use anyValue in a requirement row postcondition cell.

For example, in the model used in the Prove Properties with Requirements Table Blocks example, the table models formal requirements for an engine thrust reverser system, but it does not model the entire requirement space. When you analyze the table for modeling problems, the Analysis Results pane displays incompleteness issues..

Suppose that you are early in the process of defining requirements and want to suppress the incompleteness issues. You can define a default requirement with a postcondition of deploy == anyValue. When you analyze the table or simulate the model, the table suppresses the incompleteness issues. For more information, see anyValue.

The anyValue function does not globally suppress incompleteness issues. For example, the table will not flag the output y as incomplete when u is greater than 10, but, when you analyze the table, the block returns incompleteness issues for output y when u is greater than or equal to 0 and less than or equal to 10. To suppress the incompleteness issues create a requirement with a precondition that checks when u is greater than or equal to 0 and less than or equal to 10 and define a postcondition to check that the output y is equal to anyValue.