Model-Based Testing for Embedded Systems

388 Model-Based Testing for Embedded Systems

y

1

y′

2

y′

2

y

0

y

3

G

13

y

2

G

13

FIGURE 14.2

Hybrid automaton evolution.

Figure 14.2 illustrates the evolution of this hybrid automaton. We denote by G

ij

the

guard of the transition (q

i

,q

j

). In Figure 14.2, only the guards G

12

and G

23

are the shaded

regions. All the locations have the same staying set, which is the bounding box.

As we can see from the figure, starting from the initial state (q

1

,y

0

), the system can

generate a set of infinite number of trajectories. For instance, we consider the following

trajectories. Starting from (q

1

,y

0

), under two different continuous input functions, from the

system generates two different ...