Bounded exhaustive test input generation from hybrid invariants

Mostrar todas las versiones(2)

We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperati...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Rosner, Nicolás, Frias, Marcelo
Publicado:	2014
Materias:	Alloy Automated test generation Bounded exhaustive testing Korat SAT solving Transcoping Alloying Specifications Automated test generations SAT-solving Software testing
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15232867_v49_n10_p655_Rosner http://hdl.handle.net/20.500.12110/paper_15232867_v49_n10_p655_Rosner
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_15232867_v49_n10_p655_Rosner
record_format	dspace
spelling	paper:paper_15232867_v49_n10_p655_Rosner2023-06-08T16:19:26Z Bounded exhaustive test input generation from hybrid invariants Rosner, Nicolás Frias, Marcelo Alloy Automated test generation Bounded exhaustive testing Korat SAT solving Transcoping Alloying Specifications Automated test generations Bounded exhaustive testing Korat SAT-solving Transcoping Software testing We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declarative sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imperatively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the different alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes. We also show experiments involving collection classes that support the effectiveness of our technique, by demonstrating that (i) bounded exhaustive suites can be computed from hybrid invariants significantly more efficiently than doing so using state-of-the-art purely imperative and purely declarative approaches, and (ii) our technique is able to automatically determine efficient hybrid invariants, in the sense that they lead to an efficient computation of bounded exhaustive suites, using transcoping. Copyright © 2014 ACM. Fil:Rosner, N. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15232867_v49_n10_p655_Rosner http://hdl.handle.net/20.500.12110/paper_15232867_v49_n10_p655_Rosner
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Alloy Automated test generation Bounded exhaustive testing Korat SAT solving Transcoping Alloying Specifications Automated test generations Bounded exhaustive testing Korat SAT-solving Transcoping Software testing
spellingShingle	Alloy Automated test generation Bounded exhaustive testing Korat SAT solving Transcoping Alloying Specifications Automated test generations Bounded exhaustive testing Korat SAT-solving Transcoping Software testing Rosner, Nicolás Frias, Marcelo Bounded exhaustive test input generation from hybrid invariants
topic_facet	Alloy Automated test generation Bounded exhaustive testing Korat SAT solving Transcoping Alloying Specifications Automated test generations Bounded exhaustive testing Korat SAT-solving Transcoping Software testing
description	We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declarative sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imperatively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the different alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes. We also show experiments involving collection classes that support the effectiveness of our technique, by demonstrating that (i) bounded exhaustive suites can be computed from hybrid invariants significantly more efficiently than doing so using state-of-the-art purely imperative and purely declarative approaches, and (ii) our technique is able to automatically determine efficient hybrid invariants, in the sense that they lead to an efficient computation of bounded exhaustive suites, using transcoping. Copyright © 2014 ACM.
author	Rosner, Nicolás Frias, Marcelo
author_facet	Rosner, Nicolás Frias, Marcelo
author_sort	Rosner, Nicolás
title	Bounded exhaustive test input generation from hybrid invariants
title_short	Bounded exhaustive test input generation from hybrid invariants
title_full	Bounded exhaustive test input generation from hybrid invariants
title_fullStr	Bounded exhaustive test input generation from hybrid invariants
title_full_unstemmed	Bounded exhaustive test input generation from hybrid invariants
title_sort	bounded exhaustive test input generation from hybrid invariants
publishDate	2014
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15232867_v49_n10_p655_Rosner http://hdl.handle.net/20.500.12110/paper_15232867_v49_n10_p655_Rosner
work_keys_str_mv	AT rosnernicolas boundedexhaustivetestinputgenerationfromhybridinvariants AT friasmarcelo boundedexhaustivetestinputgenerationfromhybridinvariants
_version_	1768544793510543360

Bounded exhaustive test input generation from hybrid invariants

Ejemplares similares