Identify Inconsistent and Incomplete Formal Requirement Sets
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
.