Model-Based Testing for Embedded Systems

440 Model-Based Testing for Embedded Systems

where l is the number of hyper-edges on the path between ν

0

and ν

i

in TR(e,G)

and w

j

is the value of the label w corresponding to the concrete hyper-edge.

5. For each symbol ν

i

denoting a leaf vertex in TR(e, G) define a production rule:

ν

i

→(¬t

i

)

↑

·

c

d(ν

0

,ν

i

)+1

. (15.4)

6. Apply the production rules (15.3) and (15.4) starting from the root symbol ν

0

of TR(e,G) until all nonterminal symbols ν

i

are substituted with the terms that

include only terminal symbols t

↑

i

and d(ν

0

,ν

i

). Note that i ∈{0,...,n}, where n

is the number of trap variables in TR(e,G). The root vertex ν

0

= e of the labeled

tree TR(e,G) may not have a