Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving

Mostrar todas las versiones(3)

En muchas situaciones, el software puede recuperarse de fallas en tiempo de ejecución usando workarounds. Un workaround se define como una alternativa de ejecución para un método defectuoso que permite mantener al sistema funcionando luego de la ocurrencia de una falla. En este trabajo se presentan...

Descripción completa

Detalles Bibliográficos
Autor principal: Uva, Marcelo Ariel
Otros Autores: Ponzio, Pablo Daniel
Formato: Tesis doctoral publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2022
Materias:
RECUPERACION EN TIEMPO DE EJECUCION
WORKAROUNDS
ESPECIFICACIONES FORMALES
SAT SOLVING
RUNTIME RECOVERY
FORMAL SPECIFICATIONS
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n7251_Uva
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n7251_Uva_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-tesis_n7251_Uva_oai
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Español
orig_language_str_mv spa
topic RECUPERACION EN TIEMPO DE EJECUCION
WORKAROUNDS
ESPECIFICACIONES FORMALES
SAT SOLVING
RUNTIME RECOVERY
WORKAROUNDS
FORMAL SPECIFICATIONS
SAT SOLVING
spellingShingle RECUPERACION EN TIEMPO DE EJECUCION
WORKAROUNDS
ESPECIFICACIONES FORMALES
SAT SOLVING
RUNTIME RECOVERY
WORKAROUNDS
FORMAL SPECIFICATIONS
SAT SOLVING
Uva, Marcelo Ariel
Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving
topic_facet RECUPERACION EN TIEMPO DE EJECUCION
WORKAROUNDS
ESPECIFICACIONES FORMALES
SAT SOLVING
RUNTIME RECOVERY
WORKAROUNDS
FORMAL SPECIFICATIONS
SAT SOLVING
description En muchas situaciones, el software puede recuperarse de fallas en tiempo de ejecución usando workarounds. Un workaround se define como una alternativa de ejecución para un método defectuoso que permite mantener al sistema funcionando luego de la ocurrencia de una falla. En este trabajo se presentan dos técnicas para el cómputo automático de workarounds. Estas técnicas emplean especificaciones formales (pre y post-condiciones de métodos, e invariantes de clases), y usan SAT solving como procedimiento de decisión. A diferencia de enfoques previos, las técnicas emplean también el estado de ejecución del sistema al momento de la falla, por lo que decimos que los workarounds computados por las mismas son transitorios. En la primera técnica, los workarounds transitorios consisten de una secuencia de rutinas que satisfacen la especificación del método defectuoso, para el estado en que se produjo la falla. Se propone también un enfoque para generalizar estos workarounds transitorios a esquemas de workarounds, que sirven para acelerar la búsqueda de workarounds transitorios para otros estados que producen fallas en el método defectuoso. La segunda técnica, propone la construcción de workarounds transitorios usando SAT solving para generar directamente un estado que satisface la postcondición de la rutina defectuosa, a partir del estado donde se produjo la falla. Para optimizar esta técnica se propone usar predicados de rotura de simetrías y cotas ajustadas (técnicas del estado del arte para mejorar la eficiencia y la escalabilidad de SAT solving), y evaluar los beneficios que estos enfoques pueden brindar en el cómputo de workarounds. Las técnicas propuestas se evaluaron experimentalmente sobre una familia de casos de estudio, que incluyen implementaciones de colecciones (con estructuras de datos de distinta complejidad) y una biblioteca para aritmética de fechas. Los resultados muestran que las técnicas propuestas permiten computar workarounds transitorios en un número importante de casos, y en tiempos razonables para su aplicación a la recuperación de fallas de software en tiempo de ejecución.
author2 Ponzio, Pablo Daniel
author_facet Ponzio, Pablo Daniel
Uva, Marcelo Ariel
format Tesis doctoral
Tesis doctoral
publishedVersion
author Uva, Marcelo Ariel
author_sort Uva, Marcelo Ariel
title Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving
title_short Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving
title_full Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving
title_fullStr Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving
title_full_unstemmed Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving
title_sort cómputo automático de workarounds transitorios a partir de especificaciones de programas usando sat solving
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2022
url https://hdl.handle.net/20.500.12110/tesis_n7251_Uva
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n7251_Uva_oai
work_keys_str_mv AT uvamarceloariel computoautomaticodeworkaroundstransitoriosapartirdeespecificacionesdeprogramasusandosatsolving
AT uvamarceloariel automaticcomputationoftransientworkaroundsfromprogramspecificationsusingsatsolving
_version_ 1824355533466894336
spelling I28-R145-tesis_n7251_Uva_oai2024-09-02 Ponzio, Pablo Daniel Uva, Marcelo Ariel 2022-12-21 En muchas situaciones, el software puede recuperarse de fallas en tiempo de ejecución usando workarounds. Un workaround se define como una alternativa de ejecución para un método defectuoso que permite mantener al sistema funcionando luego de la ocurrencia de una falla. En este trabajo se presentan dos técnicas para el cómputo automático de workarounds. Estas técnicas emplean especificaciones formales (pre y post-condiciones de métodos, e invariantes de clases), y usan SAT solving como procedimiento de decisión. A diferencia de enfoques previos, las técnicas emplean también el estado de ejecución del sistema al momento de la falla, por lo que decimos que los workarounds computados por las mismas son transitorios. En la primera técnica, los workarounds transitorios consisten de una secuencia de rutinas que satisfacen la especificación del método defectuoso, para el estado en que se produjo la falla. Se propone también un enfoque para generalizar estos workarounds transitorios a esquemas de workarounds, que sirven para acelerar la búsqueda de workarounds transitorios para otros estados que producen fallas en el método defectuoso. La segunda técnica, propone la construcción de workarounds transitorios usando SAT solving para generar directamente un estado que satisface la postcondición de la rutina defectuosa, a partir del estado donde se produjo la falla. Para optimizar esta técnica se propone usar predicados de rotura de simetrías y cotas ajustadas (técnicas del estado del arte para mejorar la eficiencia y la escalabilidad de SAT solving), y evaluar los beneficios que estos enfoques pueden brindar en el cómputo de workarounds. Las técnicas propuestas se evaluaron experimentalmente sobre una familia de casos de estudio, que incluyen implementaciones de colecciones (con estructuras de datos de distinta complejidad) y una biblioteca para aritmética de fechas. Los resultados muestran que las técnicas propuestas permiten computar workarounds transitorios en un número importante de casos, y en tiempos razonables para su aplicación a la recuperación de fallas de software en tiempo de ejecución. Software failures, produced by errors in source code, can often be bypassed in run time by using the so called workarounds: execution alternatives that the system can used in place of faulty routine to circumvent the failure. In this thesis, we present two techniques for the automated computation of workarounds from Java code equipped with formal specifications (consisting of method pre and postconditions and class invariants), using SAT solving. As opposed to previous approaches, these techniques make use of the state of the system where the faulty method was executed, hence the computed workarounds are transient. In the first technique, transient workarounds are defined as an alternative set of routines that satisfy the specification of the faulty method at the given state. We propose a mechanism to generalize these transient workarounds to schemas, which can be used to speed up the search for transient workarounds in other failing states. The second technique directly exploits SAT solving to circumvent the failing method, automatically building a state that mimics its correct be- haviour (described by the method’s specification) when starting at the given state. In order to optimize and improve scalability of the second technique we compute and add symmetry breaking predicates and tight field bounds to optimize the SAT process. For the purpose of experimentally assessing the presented techniques, we develop a number of case studies based on contract-equipped collection classes and a Java library for date arithmetic. The results of the assessment show that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in times that makes them feasible to be used for run time repairs. Fil: Uva, Marcelo Ariel. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/tesis_n7251_Uva spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar RECUPERACION EN TIEMPO DE EJECUCION WORKAROUNDS ESPECIFICACIONES FORMALES SAT SOLVING RUNTIME RECOVERY WORKAROUNDS FORMAL SPECIFICATIONS SAT SOLVING Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving Automatic computation of transient workarounds from program specifications using SAT solving info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n7251_Uva_oai

Ejemplares similares