Abstraction Based Automated Test Generation from Formal Tabular Requirements Specifications

DEGIOVANNI, RENZO; PONZIO, PABLO; AGUIRRE, NAZARENO; FRIAS, MARCELO FABIAN

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: Berlín; Año: 2011 vol. 6706 p. 84 - 101

0302-9743

We propose an automated approach for generating tests from formal tabular requirements specifications, such as SCR specifications. The technique is based on counterexample guided abstraction refinement and the use of SMT solving. Moreover, in order to effectively perform au- tomated test generation, we take advantage of particular characteristics of tabular requirements descriptions to aid the abstraction and abstrac- tion refinement processes. The exploited characteristics are, most no- tably, the organisation of the requirements specification in modes, which is used to build an initial abstraction, and the execution model of tabu- lar specifications, which is directed by changes observed in environment variables and is exploited for modularising the transition relation as- sociated with tables, simplifying the calculation of abstractions. These characteristics enable us to effectively perform automated test genera- tion achieving good levels of coverage for different criteria relevant to this context. We compare our approach with a standard abstraction analysis, show- ing the benefits that exploiting the mentioned characteristics of tables provide. We also compare the approach with model checking based gen- eration, using several model checking tools. Our experiments show that the presented approach is able to generate test cases from models whose complexity, with respect to the sizes of variables and data domains, can- not be coped with well by the model checkers we used.