Model-Based Testing for Embedded Systems

176 Model-Based Testing for Embedded Systems

TABLE 7.1

The Use of the Operators when and current

E e

0

e

1

e

2

e

3

e

4

e

5

e

6

e

7

e

8

...

B false false true false true false false true true ...

X=E when B x

0

= e

2

x

1

= e

4

x

2

= e

7

x

3

= e

8

...

Y=current(X) y

0

= nil y

1

= nil y

2

= e

2

y

3

= e

2

y

4

= e

4

y

5

= e

4

y

6

= e

4

y

7

= e

7

y

8

= e

8

...

node ex2cks(m:int) returns (c:bool; y:int);

var (x:int) when c;

let

y = if c then current(x) else pre(y)-1;

c = true -> (pre(y)=0);

x = m when c;

tel;

−

ITE

=

pre

when

current

x

M1

M51

y

M2

M3

0

True

M4

c

m

FIGURE 7.5

The

ex2cks example and the corresponding operator network; two clocks are used, the basic

clock and the flow c.

The sampling and the projection are two complementary operations: ...