The Feasibility of Automated Feedback-Directed Test Generation: A Case Study of a High-Assurance Operating System

In this paper, we describe results of a case study to establish the feasibility of deriving mappings between an abstract user level specification and the concrete implementation. Such a mapping is necessary for feedback-directed testing to improve code coverage, needed by the stringent criteria for high-assurance systems. In particular, our work focused on establishing mappings between an abstract user level specification and uncovered code elements in the implementation of a highly secure smart card operating system. We used test cases generated from the user level specification to identify the executed code elements and attempted to use static analysis to map the unexecuted code elements to the corresponding elements in the user level specification.

Our primary result is evidence that, given a sufficiently expressive user level specification and a test generation system that is able to effectively use such a specification, 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 inferring the semantics of the internal implementation of data structures. In particular, we observed that the internal states at the implementation level in a high security application pose significant challenges to this mapping process.


By: Sam Weber; Suzanne K. McIntosh; Amitkumar Paradkar; David C. Toll; Paul A. Karger; Matthew Kaplan; Elaine R. Palmer

Published in: The Feasibility of Automated Feedback Directed Specification-Based Test Generation: A Case Study of a High-Assurance Operating SystemSeattle/Redmond, WA, IEEE, p.229-38 in 2008

Please obtain a copy of this paper from your local library. IBM cannot distribute this paper externally.

Questions about this service can be mailed to .