Model-Based Testing for Embedded Systems

478 Model-Based Testing for Embedded Systems

A variant of the well-known Collatz algorithm (after the mathematician Lothar Collatz,

1910–1990), can be defined in pseudo code as follows:

INPUT natural number N > 0.

WHILE (N > 1)

{IF (N even number)

THEN { N:=N/2}

ELSE { N:=(3*N)+1}}

HALT.

If Collatz’s famous conjecture (1937, still unproven to date) is true, then this algorithm will

eventually terminate (halt) for any (every) given input from the natural numbers.

Let us now try to apply our method of passive testing to Collatz’s algorithm and inject

trace-emitting instructions at its crucial points, as follows:

INPUT natural number N > 0.

WHILE (N > 1)

{IF (N even number)

THEN { N := N/2 ; PRINT(“down”) }

ELSE { N:=(3*N)+1} ; PRINT(“up”) }

HALT.

Under the assumption ...