Bounded Exhaustive Search of Alloy Specification Repairs

Mostrar todas las versiones(2)

The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite significant advances in program repair for imperative languages, there is a dearth of repair techniques for dec...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Gutiérrez Brida, Simón, Regis, Germán, Zheng, Guolong, Bagheri, Hamid, Nguyen, ThanhVu, Aguirre, Nazareno Matías, Frias, Marcelo F.
Formato: Objeto de conferencia Resumen
Lenguaje:Inglés
Publicado: 2021
Materias:
Ciencias Informáticas
Metals
Maintenance engineering
Tools
Syntactics
Software
Space exploration
Task analysis
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/140426
http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-09.pdf
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-140426
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Metals
Maintenance engineering
Tools
Syntactics
Software
Space exploration
Task analysis
spellingShingle Ciencias Informáticas
Metals
Maintenance engineering
Tools
Syntactics
Software
Space exploration
Task analysis
Gutiérrez Brida, Simón
Regis, Germán
Zheng, Guolong
Bagheri, Hamid
Nguyen, ThanhVu
Aguirre, Nazareno Matías
Frias, Marcelo F.
Bounded Exhaustive Search of Alloy Specification Repairs
topic_facet Ciencias Informáticas
Metals
Maintenance engineering
Tools
Syntactics
Software
Space exploration
Task analysis
description The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite significant advances in program repair for imperative languages, there is a dearth of repair techniques for declarative languages. We present BeAFix, an automated repair technique for faulty models written in Alloy, a first-order relational logic language. BeAFix has a number of distinguishing features. Firstly, it supports any kind of oracle, including assertions typically found in formal specifications, as well as “specification tests”. This is important since unit tests, widely available for programs, are not typically found in formal specifications. Secondly, given a defined set of mutation operations, a set of suspicious expressions and a maximum number of mutations to apply per expression, BeAFix's bounded-exhaustive approach will either find a fix, or guarantee that such a fix is not possible, within the provided bounds. With respect to fault localization, BeAFix is not tightly integrated to any specific technique. In fact, our technique is independent of the fault localization technique used, and the fault localization is run only once before the repair process begins. To support a bounded-exhaustive approach while keeping repair times reasonable, sound state pruning techniques (i.e., those that guarantee that no valid fixes are removed) are introduced. When a faulty model has more than one suspicious expression, we use both syntactic analysis and dynamically generated scenario-based assertions to check the feasibility of a particular repair candidate. A failing check will determine that this candidate would never lead to a fully repaired model, allowing BeAFix to prune significant parts of the search space. We evaluated our technique on two Alloy benchmarks, including one previously used in a state-of-the-art technique for Alloy repair. The results show that BeAFix is able to repair thousands of real-world faulty models, corroborating its ability to effectively, and efficiently generate correct repairs while also being less prone to overfitting than previous techniques.
format Objeto de conferencia
Resumen
author Gutiérrez Brida, Simón
Regis, Germán
Zheng, Guolong
Bagheri, Hamid
Nguyen, ThanhVu
Aguirre, Nazareno Matías
Frias, Marcelo F.
author_facet Gutiérrez Brida, Simón
Regis, Germán
Zheng, Guolong
Bagheri, Hamid
Nguyen, ThanhVu
Aguirre, Nazareno Matías
Frias, Marcelo F.
author_sort Gutiérrez Brida, Simón
title Bounded Exhaustive Search of Alloy Specification Repairs
title_short Bounded Exhaustive Search of Alloy Specification Repairs
title_full Bounded Exhaustive Search of Alloy Specification Repairs
title_fullStr Bounded Exhaustive Search of Alloy Specification Repairs
title_full_unstemmed Bounded Exhaustive Search of Alloy Specification Repairs
title_sort bounded exhaustive search of alloy specification repairs
publishDate 2021
url http://sedici.unlp.edu.ar/handle/10915/140426
http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-09.pdf
work_keys_str_mv AT gutierrezbridasimon boundedexhaustivesearchofalloyspecificationrepairs
AT regisgerman boundedexhaustivesearchofalloyspecificationrepairs
AT zhengguolong boundedexhaustivesearchofalloyspecificationrepairs
AT bagherihamid boundedexhaustivesearchofalloyspecificationrepairs
AT nguyenthanhvu boundedexhaustivesearchofalloyspecificationrepairs
AT aguirrenazarenomatias boundedexhaustivesearchofalloyspecificationrepairs
AT friasmarcelof boundedexhaustivesearchofalloyspecificationrepairs
bdutipo_str Repositorios
_version_ 1764820458812735490

Ejemplares similares