Coverage Criteria for Set-Based Specifications

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

REVISTA DE INFORMATICA TEORICA E APLICADA

Instituto de Informática - UFRGS

Año: 2015 vol. 22 p. 316 - 335

0103-4308

Model-based testing (MBT) studies how test cases are generated froma model of the system under test (SUT). Many MBT methods rely on building an au-tomaton from the model and then they generate test cases by covering the automatonwith different path coverage criteria. However, if a model of the SUT is a logical for-mula over some complex mathematical theories (such as set theory) it may be morenatural or intuitive to apply coverage criteria directly over the formula. On the otherhand, domain partition, i.e. the partition of the input domain of model operations, isone of the main techniques in MBT. Partitioning is conducted by applying differentrules or heuristics. Engineers may find it difficult to decide what, where and how theserules should be applied. In this paper we propose a set of coverage criteria based ondomain partition for set-based specifications. We call them testing strategies. Testingstrategies play a similar role to path- or data-based coverage criteria in structural test-ing. Furthermore, we show a partial order of testing strategies as is done in structuraltesting. We also describe an implementation of testing strategies for the Test TemplateFramework, which is a MBT method for the Z notation; and a language that allowsuser to implement testing strategies.