
200 Model-Based Testing for Embedded Systems
8.2.1 Definition of the behaviors
A behavior is a subpart of an operation that represents one possible effect of the operation.
Each behavior can be defined as a predicate, representing its activation condition, and a
substitution that represents its effect, namely the evolution of the state variables and the
instantiation of the return parameters of the operation. The behaviors are computed as the
paths in the control flow graph of the considered B operation, represented as a before–after
predicate.
∗
Example 1 (Computation of behaviors). Consider a smart card command, named
VERIFY
PIN aimed at checking a PIN co ...