Using LTL rewriting to improve the performance of model-checker based test-case generation

Model-checkers have recently been suggested for automated software test-case generation. Several works have presented methods that create efficient test-suites using model-checkers. Ease of use and complete automation are major advantages of such approaches. However, the use of a model-checker comes at the price of potential performance problems. If the model used for test-case generation is complex, then model-checker based approaches can be very slow, or even not applicable at all. In this paper, we identify that unnecessary, redundant calls to the model-checker are one of the causes of bad performance. To overcome this problem, we suggest the use of temporal logic rewriting techniques, which originate from runtime verification research. This achieves a significant increase in the performance, and improves the applicability of model-checker based test-case generation approaches in general. At the same time, the suggested techniques achieve a reduction of the resulting test-suite siz...

• Type: Conference
• Year: 2007
• Where: AMOST
• Authors: Gordon Fraser, Franz Wotawa
• Keywords: AMOST 2007, Austrian Federal Ministry, Software Engineering, Software Test-case Generation, Test-case Generation