The Feasibility of Automated Feedback-Directed Test Generation

SUPERSEDED BY RC24547.

In this paper, we describe results of an experiment to establish feasibility of deriving mappings between abstract specification and concrete implementation. Such a mapping is necessary for feedback driven testing in order to satisfy stringent criteria for high assurance systems. In particular, our work focused on establishing mappings between abstract specification and uncovered code elements in the concrete implementation of a highly secure smartcard operating system. Our primary result is evidence that, given a sufficiently expressive model and a test generation system that is able to effectively use such a model, the resulting tests will cover the vast majority of the code branches that are able to be covered. Therefore, the benefit of a feedback-directed system will be limited. We, further, provide evidence that the static analysis required to generate feedback in these cases tends to be difficult, involving infering the semantics of internal implementation data structures.