Model-Based Testing for Embedded Systems

Functional Test Generation 43

which must have the value p

1

from (2.5) in order for ψ

2

to return true because the predicate

ψ

2

was derived assuming that input in the first place. However, there is no guarantee that

the component A will produce output p

2

when given the input m

1

as the only guaranteed

assertion is that the output after m

1

fulfills φ

2

, while φ

2

and p

1

do not necessarily have any

relationship to each other as they come from two independent and separate models.

This discussion has so far focused on that compositionality breaks for tester models that

do not predict system outputs fully. The other problem mentioned previously was that tester

models do ...