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

Uva, Marcelo Ariel

Registro:

Documento:	Tesis Doctoral
Título:	Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving
Título alternativo:	Automatic computation of transient workarounds from program specifications using SAT solving
Autor:	Uva, Marcelo Ariel
Editor:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Filiación:	Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas Físico-Químicas y Naturales. Departamento de Computación
Publicación en la Web:	2023-04-03
Fecha de defensa:	2022-12-21
Fecha en portada:	21 de diciembre de 2022
Grado Obtenido:	Doctorado
Título Obtenido:	Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación
Director:	Ponzio, Pablo Daniel
Director Asistente:	López Pombo, Carlos Gustavo
Consejero:	Galeotti, Juan Pablo
Jurado:	Pons, Claudia; Demasi, Ramiro; Marcos, Claudia
Idioma:	Español
Palabras clave:	RECUPERACION EN TIEMPO DE EJECUCION; WORKAROUNDS; ESPECIFICACIONES FORMALES; SAT SOLVINGRUNTIME RECOVERY ; WORKAROUNDS; FORMAL SPECIFICATIONS; SAT SOLVING
Formato:	PDF
Handle:	http://hdl.handle.net/20.500.12110/tesis_n7251_Uva
PDF:	https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n7251_Uva.pdf
Registro:	https://bibliotecadigital.exactas.uba.ar/collection/tesis/document/tesis_n7251_Uva
Ubicación:	Dep.COM 007251
Derechos de Acceso:	Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Uva, Marcelo Ariel. (2022). Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/tesis_n7251_Uva

Resumen:

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.

Abstract:

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.

Citación:

---------- APA ----------

Uva, Marcelo Ariel. (2022). Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/tesis_n7251_Uva

---------- CHICAGO ----------

Uva, Marcelo Ariel. "Cómputo automático de workarounds transitorios a partir de especificaciones de programas usando SAT solving". Tesis Doctoral, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2022.https://hdl.handle.net/20.500.12110/tesis_n7251_Uva

Estadísticas:

Descargas totales desde :

Navegar

Colección

Tesis Doctoral