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.
THIS REPORTS SUPERSEDES RC24355
By: Sam Weber; Suzanne K. McIntosh; Amitkumar Paradkar; David C. Toll; Paul A. Karger; Matthew Kaplan; Elaine R. Palmer
Published in: RC24547 in 2008
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .
