Automated workarounds from Java Program specifications based on SAT solving

"The failures that bugs in software lead to can sometimes be bypassed by the so called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Previous works have exploited this workarounds noti...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Uva, Marcelo, Ponzio, Pablo, Regis, Germán, Aguirre, Nazareno, Frías, Marcelo
Formato: Ponencias en Congresos publishedVersion
Lenguaje:Inglés
Publicado: 2020
Materias:
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/3066
Aporte de:
id I32-R138-123456789-3066
record_format dspace
spelling I32-R138-123456789-30662022-12-07T14:13:57Z Automated workarounds from Java Program specifications based on SAT solving Uva, Marcelo Ponzio, Pablo Regis, Germán Aguirre, Nazareno Frías, Marcelo ANALISIS DE FALLAS ESPECIFICACIONES DEPURACION DE PROGRAMAS LENGUAJES DE PROGRAMACION SOFTWARE JAVA "The failures that bugs in software lead to can sometimes be bypassed by the so called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Previous works have exploited this workarounds notion to automatically recover from runtime failures in some application domains. However, existing approaches that compute workarounds automatically either require the user to manually build an abstract model of the software under consideration, or to provide equivalent sequences of operations from which workarounds are computed, diminishing the automation of workaround-based system recovery. In this paper, we present two techniques that automatically compute workarounds from Java code equipped with formal specifications, avoiding abstract software models and user provided equivalences. These techniques employ SAT solving to compute workarounds on concrete program state characterizations. The first employs SAT solving to compute traditional workarounds, while the second directly exploits SAT solving to circumvent a failing method, building a state that mimics the (correct) behaviour of this failing routine. Our experiments, based on case studies involving implementations of collections and a library for date arithmetic, enable us to show that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run time repairs." 2020-09-28T18:49:14Z 2020-09-28T18:49:14Z 2017 Ponencias en Congresos info:eu-repo/semantics/publishedVersion 1433-2787 http://ri.itba.edu.ar/handle/123456789/3066 en info:eu- repo/semantics/reference/doi.org/10.1007/s10009-018-0503-8 application/pdf
institution Instituto Tecnológico de Buenos Aires (ITBA)
institution_str I-32
repository_str R-138
collection Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA)
language Inglés
topic ANALISIS DE FALLAS
ESPECIFICACIONES
DEPURACION DE PROGRAMAS
LENGUAJES DE PROGRAMACION
SOFTWARE
JAVA
spellingShingle ANALISIS DE FALLAS
ESPECIFICACIONES
DEPURACION DE PROGRAMAS
LENGUAJES DE PROGRAMACION
SOFTWARE
JAVA
Uva, Marcelo
Ponzio, Pablo
Regis, Germán
Aguirre, Nazareno
Frías, Marcelo
Automated workarounds from Java Program specifications based on SAT solving
topic_facet ANALISIS DE FALLAS
ESPECIFICACIONES
DEPURACION DE PROGRAMAS
LENGUAJES DE PROGRAMACION
SOFTWARE
JAVA
description "The failures that bugs in software lead to can sometimes be bypassed by the so called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Previous works have exploited this workarounds notion to automatically recover from runtime failures in some application domains. However, existing approaches that compute workarounds automatically either require the user to manually build an abstract model of the software under consideration, or to provide equivalent sequences of operations from which workarounds are computed, diminishing the automation of workaround-based system recovery. In this paper, we present two techniques that automatically compute workarounds from Java code equipped with formal specifications, avoiding abstract software models and user provided equivalences. These techniques employ SAT solving to compute workarounds on concrete program state characterizations. The first employs SAT solving to compute traditional workarounds, while the second directly exploits SAT solving to circumvent a failing method, building a state that mimics the (correct) behaviour of this failing routine. Our experiments, based on case studies involving implementations of collections and a library for date arithmetic, enable us to show that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run time repairs."
format Ponencias en Congresos
publishedVersion
author Uva, Marcelo
Ponzio, Pablo
Regis, Germán
Aguirre, Nazareno
Frías, Marcelo
author_facet Uva, Marcelo
Ponzio, Pablo
Regis, Germán
Aguirre, Nazareno
Frías, Marcelo
author_sort Uva, Marcelo
title Automated workarounds from Java Program specifications based on SAT solving
title_short Automated workarounds from Java Program specifications based on SAT solving
title_full Automated workarounds from Java Program specifications based on SAT solving
title_fullStr Automated workarounds from Java Program specifications based on SAT solving
title_full_unstemmed Automated workarounds from Java Program specifications based on SAT solving
title_sort automated workarounds from java program specifications based on sat solving
publishDate 2020
url http://ri.itba.edu.ar/handle/123456789/3066
work_keys_str_mv AT uvamarcelo automatedworkaroundsfromjavaprogramspecificationsbasedonsatsolving
AT ponziopablo automatedworkaroundsfromjavaprogramspecificationsbasedonsatsolving
AT regisgerman automatedworkaroundsfromjavaprogramspecificationsbasedonsatsolving
AT aguirrenazareno automatedworkaroundsfromjavaprogramspecificationsbasedonsatsolving
AT friasmarcelo automatedworkaroundsfromjavaprogramspecificationsbasedonsatsolving
_version_ 1765660985733939200