untitled

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

Uva, Marcelo Ariel

Director(a):
Ponzio, Pablo Daniel
 
Institución otorgante:
Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Fecha:
2022-12-21
Tipo de documento: 
info:eu-repo/semantics/doctoralThesis
 
Formato:
application/pdf
Idioma:
spa
Temas:
RECUPERACION EN TIEMPO DE EJECUCION - WORKAROUNDS - ESPECIFICACIONES FORMALES - SAT SOLVING - RUNTIME RECOVERY - WORKAROUNDS - FORMAL SPECIFICATIONS - SAT SOLVING
Descripción:
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.
Identificador:
https://hdl.handle.net/20.500.12110/tesis_n7251_Uva
Derechos:
info:eu-repo/semantics/openAccess
http://creativecommons.org/licenses/by-nc-nd/2.5/ar/
Licencia de uso:
Licencia Creative Commons

Descargar texto: tesis_n7251_Uva.oai

Cita bibliográfica:

Uva, Marcelo Ariel  (2022-12-21).     Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving.  (info:eu-repo/semantics/doctoralThesis).    Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.    [consultado:  23/1/2025] Disponible en el Repositorio Digital Institucional de la Universidad de Buenos Aires:  <https://hdl.handle.net/20.500.12110/tesis_n7251_Uva>


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27