Coverage Criteria for Logical Specifications

CRISTIÁ, MAXIMILIANO; CUENCA, JOAQUÍN; FRYDMAN, CLAUDIA

Maceió

Workshop; 8th Brazilian Workshop on Systematic and Automated Software Testing (SAST'14); 2014

Model-based testing (MBT) studies how to generate test cases from a model of the system under test (SUT). Many MBT methods rely on building an automaton from the model and then they generate test cases by covering the automaton with different path coverage criteria. However, if a model of the SUT is a logical formula over some complex mathematical theories (such as the Z notation) it may be more natural or intuitive to apply coverage criteria directly over the formula. In this paper we propose a set of coverage criteria for logical specifications based on domain partition. We call them testing strategies. Testing strategies play a similar role to path- or data-based coverage criteria. Furthermore, we show a partial order of testing strategies as is done in structural testing. We also describe an implementation of testing strategies for the Test Template Framework, which is a MBT method for the Z notation.