Engineering the Development of Embedded Systems - Formal Methods and Hybrid Real-Time Systems - page 397

Much work has been done on the use of program analysis for static testing of pro-
grams. While a great deal of progress has been made on static testing, especially for
unit testing, such methods are inherently limited:

1. Unit testing requires a test harness to be created to substitute for the actual execu-
tion environment of the unit;
2. Representative test values need to be computed to ensure that all control paths in
the unit are traversed.

Both of these are time-consuming, even if done using a test generation tool. There is
therefore a strong temptation to do perfunctory unit test, or to skip the stage altogether.
Unit testing must be followed by module and system testing, where new test data
must be generated. This is altogether more difficult because it involves testing the func-
tionality of the program as execution passes through various modules and units. Sys-
tematic test may attempt to be comprehensive but still fail to perform the boundary tests
(the corner cases) which are often the cause of errors.
[Godefroid et al 2005] show how dynamic testing can be used for testing software.
The method automatically generates a test harness for the program, randomly generates
test values and analyses the results to be able to generate new values that will exercise
the program in different ways. Later work ([Godefroid 2007]) extends the results to
allow testing to be done compositionally, by testing a unit in a test environment that
makes use of the results of the tests of the other units in the program. This makes
testing truly scalable, since it allows testing of new or modified units without re-testing
of all the units with which it interfaces.
Godefroid's techniques for random testing could be used to develop an effective
method for testing an embedded program statically, before it is integrated into a system
and tested.

10 Conclusions

The field of embedded systems has grown enormously over the past two decades with
a wide variety of applications. Programming techniques have also developed but there
are several areas where formal analysis is still very difficult or not possible at all using
current methods. There are numerous problems that need further study, ranging from
requirements validation to processor design.
It would be an apt tribute to the work initiated here by Dines Bjørner and Zhou
Chaochen to embark on an investigation of these problems.

Acknowledgements

A number of people have commented on an earlier version of this material which was
presented as an invited talk at the First Conference on Theory and Applications of
Software Engineering in Shanghai [Joseph 2007]. I have benefited from discussions
with R. Venkatesh, Vivek Diwanji and Zhiming Liu. Joseph Sifakis has sent a number
of very useful comments. My thanks to all of them.