Model-Based Testing for Embedded Systems

186 Model-Based Testing for Embedded Systems

There are four operators specifically introduced for testing purposes:

1. The

environment operator makes it possible to specify invariant properties of the

program environment.

2. The

prob operator is used to define conditional probabilities. The expression

prob(C,E,P) means that if the condition C holds, then the probability of the ex-

pression

E to be true is equal to P.

3. The

safeprop operator is exploited by Lutess to guide the test generation toward

situations that could violate the program safety properties (see safety-property-

guided testing).

4. The

hypothesis operator introduces knowledge or assumptions in the test gener-

ation process targeting to improve the fault-detection ability of safety-property- ...