Model-Based Testing for Embedded Systems

Functional Test Generation 33

of the output tape correspond to the system’s output. We assume that all system models

eventually halt on all inputs.

∗



The next definition fixes the model-based test coverage criteria considered within the

rest of this section.

Definition 3 (Output Transition). Given a system model, an output transition in the

system model is a q,σ

i

,σ

o

,σ iff δ(q,σ

i

,σ

o

,σ) is defined (the machine can take a step

forward) and the transition moves the head on the output tape right (thus committing the

machine to a new output symbol). A halting

†

run of a system models covers an output

transition if a configuration matching an output transition shows ...