Model-Based Testing for Embedded Systems

Model-Based Passive Testing of Safety-Critical Components 463

an abstract state machine with operations and invariants. B specifications can be written

nondeterministically on a high level of abstraction, but can be refined to more specific

deterministic specifications. In such a deterministic form, B models can be made executable

and thus serve the purpose of rapid prototyping, or—as in the case of Howard et al. (2003)—

the generation and analysis of runtime traces.

Indeed, it is interesting to note that testing by trace checking in Howard et al. (2003)

was done only in an indirect, not in a direct fashion. The checked traces were in fact not

the traces of the web-based system that was mentioned above, which we could call in hind-

sight the “primary” ...