Model-Based Testing for Embedded Systems

Test Generation Using Symbolic Animation of Models 215

help filtering the resulting tests according to various criteria (test length, cycle coverage,

etc.). The conformance is established using the ioco (Tretmans 1996) relationship. The

major differences with our automated approach is that, first, we do not know the topology

of the system. As a consequence, the treatment of the model differs. Second, these processes

are based on the online (or on-the-fly) testing paradigm in which the model program and

the implementation are considered together. On the contrary, our approach is amenable

to offline testing that requires a concretization step for the tests to be run on the SUT

and the conformance to be established. Notice that the online testing approaches ...