7. Reactis Assertions#

Reactis uses assertions to find test cases which result in a run-time error or other incorrect model behavior. An assertion is a condition which must always be true for a model to execute correctly. For example, if a block B calculates the quotient x/y for integer inputs x and y, it must never be the case that y is zero. Hence, an assertion for the block B could be informally stated as “y is not zero when B is executed.” If this assertion is ever false, then we know a division-by-zero error will occur when the block B is executed.

There are three basic kinds of assertion in Reactis.

Run-time error assertions.

These assertions are automatically generated by Reactis and are used to find common run-time errors. They are described in more detail in the Run-Time Error Assertions section.

User-defined assertions.

You can create your own assertions to check that more complex conditions are always true for a model. These are described in more detail in the User-Defined Assertions section.

Excluded target assertions.

These assertions check that a target which has been excluded from coverage tracking is in fact never covered. They are described in more detail in the Excluded Target Assertions section.

7.1. Run-Time Error Assertions#

A run-time error assertion (RTE assertion) is an assertion which is automatically generated by Reactis to check for a common run-time error. There are several categories of run-time error assertion:

Indexing.

An assertion which checks that the value of an index passed into a Multiport Switch block is out of range. One indexing assertion is created for each Multiport Switch block.

Integer overflow.

An assertion which checks that the result of a basic integer or fixed-point operation lies within the bounds allowed by the result type of the operation. For example, if a calculation x + y is performed with result type int16 (which can represent values in the range −32768 … 32767), then the RTE assertion for x + y is −32768 ≤ (x + y) ≤ 32767. An integer overflow assertion is created for each of the following blocks when saturate on integer overflow is turned off.

  • Abs

  • Add

  • Divide

  • Gain

  • Product

  • Product of Elements

  • Subtract

  • Sum

  • Sum of Elements

  • Unary Minus

  • Data Type Conversion from any type to an integer or fixed-point type

Integer division by zero.

An assertion which checks that the divisor in an integer or fixed-point division expression is not zero. For example, the RTE assertion for the expression x ÷ y is y ≠ 0. An integer division by zero assertion is created for the following blocks when their datatype settings are configured such that an integer division operation occurs:

  • Divide

  • Product

  • Product of Elements

Inf/NaN.

An assertion which checks that the result of a floating-point operation is neither infinite (Inf) nor not-a-number (NaN). In other words, the Inf/NaN assertion checks that the result of the operation is a finite value. For example, if x and y are both 0.0, the result of x ÷ y would be NaN, which would result in an assertion violation. An assertion is created for a block of the following types if it performs a floating-point operation which can potentially produce an Inf or NaN result. This includes multiplication, division, addition, subtraction, and data type conversions from a larger floating-point type to a smaller floating-point type.

  • Add

  • Divide

  • Gain

  • Product

  • Product of Elements

  • Subtract

  • Sum

  • Unary Minus

  • Sum

  • Gain

  • Product

  • Data type conversion from any type to a floating-point type.

7.2. User-Defined Assertions#

User-defined assertions are assertions which are created using Reactis Validator and can be used to check any condition which should always hold true. For example, if a subsystem block produces outputs x and y, and it should always be the case that x is greater than y, then you can add the assertion x > y to your model with Reactis Validator. The process for creating user-defined assertions is explained in more detail in the Reactis Validator chapter.

7.3. Excluded Target Assertions#

An excluded target assertion is generated for targets which have been excluded from coverage tracking using the option Exclude target from coverage tracking and monitor via assertion, as shown in Figure 6.22. See the Excluding Individual Targets section for more detail on how to exclude a individual target from coverage tracking.

7.4. How Assertions Impact Testing#

The presence of assertions in a model impacts how Reactis works in a number of ways. The impacts are the same for both RTE assertions generated by Reactis and user-created Validator assertions.

First, whenever a model executes in Simulator or Tester, Reactis tracks the status of each assertion. There are three possible values for the status of an assertion:

Impossible to violate

Reactis has statically determined that the assertion cannot be violated.

Violated

Reactis has found a test that leads to the violation of the assertion.

Not violated

Reactis has neither proved the assertion is impossible to violate, nor found any test step in which the assertion is violated. In some places, Reactis reports this status as “Ok” which is equivalent to “not violated”.

When Simulator or Tester start, a static analysis is preformed that checks each assertion to determine if it is impossible to violate the assertion. For example, if a non-zero constant value is used as the divisor input to an integer divide block D, then it is impossible for D to ever perform a division by zero, and henceforth we know that the assertion “D does not perform a division by zero” will never be violated during any possible execution scenario. In cases like this, Reactis will mark the assertion as “impossible to violate”. The analysis performed by Reactis is a conservative analysis which is not guaranteed to find all assertions which can never be violated. In other words, there may be some assertions which can never be violated but are not marked as “impossible to violate” Reactis.

For every assertion which is not impossible to violate, Reactis Tester attempts to select a sequence of inputs that cause the assertion to be false. If such a test is found, the assertion will be marked as “violated” and the test leading to the violation will be included in the generated test suite.

Reactis reports the status of assertions in a number of different ways. The main panel identifies RTE assertions and Validator assertions as shown in Figure 7.1. When Simulator is enabled, violated assertions are drawn with a red foreground and yellow background. Hovering over a check mark or lightning bolt reports if the assertion has been violated and the test/step number when the violation occurred.

_images/assertions.png

Fig. 7.1 In the main Reactis panel, a circled check mark is drawn at the upper right corner of each Simulink block which has an associated RTE assertion. Validator assertions are drawn as a lightning bolt.#

Additionally, summary statistics for all assertion categories are presented at the bottom of the Coverage Summary window (item 2 in Figure 8.15). Assertion summaries are also included in the Coverage Report Browser (item 3 in Figure 11.1) and exported HTML reports (the bottom portion of Figure 11.3).