Técnicas automáticas para la diagnosis de errores en software diseñado por contrato

Resumen

Cada vez más la calidad en los productos software es primordial. En el desarrollo del software los costes asociados a la reparación de los errores representan un porcentaje importante de recursos, por tanto, mejorar el proceso de reparación de dichos errores permitirí ;a obtener un ahorro significativo en el coste final del producto software. La reparación de errores no sólo está presente en el desarrollo, sino también en el mantenimiento, si tenemos en cuenta que muchos de los productos software desarrollados sufrirán cambios durante su vida útil para poder adaptarse a los nuevos requisitos que se presenten. En esta tesis se propone una metodología para la identificación automática de defectos en el software, evitando el gasto de recursos que conllevaría la identificación de los defectos de manera manual. La metodología propuesta, denominada Diagnosis del Software Basada en Modelos de Restricciones, puede ser aplicada en el desarrollo del software y también durante el mantenimiento del software. Se basa en la combinación de diferentes paradigmas, tales como: la Diagnosis Basada en Modelos, la Programación con Restricciones, la generación de pruebas, y el Diseño por Contrato. Tiene por objetivo localizar e identificar de forma automática la causa de los errores de una aplicación software. Permite actuar sobre los asertos que forman el Diseño por Contrato y sobre las sentencias que forman el código fuente. Con respecto a los asertos, la metodología permite comprobar si la especificación ´on contiene inconsistencias, y si las contiene, permite identificar qué defectos semánticos han dado lugar a dichas inconsistencias. Con respecto a las sentencias, la metodología permite identificar cuáles son los defectos semánticos del código fuente que han provocado que determinados casos de prueba no produzcan los resultados correctos. Los defectos son semánticos cuando la especificación o el código fuente pueden ejecutarse, pero sin embargo no se producen los resultados correctos. Es decir, los defectos son debidos a un mal diseño de la especificación o del código fuente, y por tanto, los asertos de la especificación o las sentencias del código fuente deben cambiar para poder generar los resultados correctos. La metodología se basa en la aplicación secuencial de tres pasos:1. La generación automática del modelo basado en restricciones del sistema software a partir de la especificación o código fuente.2. Detección automática de inconsistencias a partir del modelo y casos de prueba.3. Identificación automática de posibles defectos a partir del modelo y casos de prueba.