Model-Based Testing for Embedded Systems

Test Generation Using Symbolic Animation of Models 205

Coverage criterion). Rewriting 2 produces two test targets, one considering the satisfaction

of P

1

, and the other the satisfaction of P

2

. Rewriting 3 will also produce two test targets,

considering an exclusive satisfaction of P

1

without P

2

and vice versa. Finally, Rewriting 4

produces three test targets that will cover all the possibilities to satisfy the disjunctions.

Notice that the consistency of the resulting test targets is checked so as to eliminate

inconsistent test targets.

Example 5 (Decision coverage). Consider behavior [1,2,9,0] from operation VERIFY_PIN

presented in Figure 8.3. The