Twice rewritings to reduce test case generation with model checker

Abstract

Generating test cases with a model checker provides an effective means to perform test automation. However, there are usually much redundant calls to the model checker such that degrade the performance of test case generation, and also the generated test suit is often much redundant. In this paper, we propose a reduction approach to test case generation by using property rewriting technique. The approach includes twice rewritings: one is for eliminating redundant test goals represented in LTL properties, and the other for eliminating redundant test cases. A simple example, withdrawing money from ATM, is employed to illustrate our approach. © 2012 Springer-Verlag GmbH.