Case Study: Automatic Test Case Generation for a Secure Cache Implementation

摘要

While many approaches for automatic test case generation have been proposed over the years, it is often difficult to predict which of them may work well on concrete problems. In this paper, we therefore present a case study in automatic, model-based test case generation: We implemented several graph-based methods that compute test cases with a model checker using trap properties, and evaluate these methods on a Secure Block Device implementation. We compare the number of generated test cases, the required generation time and the achieved code coverage. Our conclusions are twofold: First, automatic test case generation is feasible and beneficial for this case study, and even found a real bug in the implementation. Second, simple coverage methods on the model may already yield test suites of sufficient quality.