Slicing slices, an incremental backward trace slicing methodology for rwl computations

Abstract

[EN] Execution traces are an important source of information for program understanding and debugging. However, they have as an important drawback that they are commonly huge and complex, making their manual analysis unfeasible. In this master's thesis, we develop a trace slicing technique for rewriting logic computations together with its corresponding implementation in the iJulienne graphical tool. Such technique gives support to the analysis of complex, textually-large system computations in rewriting logic, which is a general framework efficiently implemented in the Maude language. Given a Maude execution trace T and a slicing criterion for the trace (i.e., a piece of information that we want to observe in the final computation state), we traverse T from back to front and the backward dependence of the observed information is incrementally computed at each execution step. At the end of the traversal, a simplified trace slice is obtained by filtering out all the irrelevant data that do not impact on the data of interest. By simplifying the trace, the iJulienne tool, which implements the proposed trace slicing technique, favors better inspection and debugging activities. iJulienne is also endowed with a trace querying mechanism that increases flexibility and reduction power and allows program runs to be examined at the appropriate level of abstraction

[ES] Las trazas de ejecución son una importante fuente de información para el entendimiento y depuración de los programas. Sin embargo, poseen el importante inconveniente de ser habitualmente enormes y complejas, haciendo inviable su análisis manual. En esta tesis de máster se ha desarrollado una técnica de fragmentación de trazas para computaciones en lógica de reescritura junto con su correspondiente implementación en la herramienta gráfica iJulienne. Dicha técnica da soporte al análisis de extensas y complejas computaciones en lógica de reescritura, que es un marco formal muy general eficientemente implementado en el lenguaje Maude. Dada una traza de ejecución de Maude T y un criterio de fragmentación para la traza (es decir, un fragmento de información que se desea observar en el estado final de la computación), nuestra técnica recorre T de atrás hacia adelante a la vez que calcula la dependencia hacia atrás de la información observada de forma incremental en cada paso de ejecución. Al final del recorrido se obtiene una traza fragmentada simplificada al filtrar toda la información irrelevante que no afecta a los datos de interés. Al simplificar la traza, la herramienta iJulienne, que implementa la técnica de fragmentado propuesta, favorece un mejor análisis y depuración de las trazas manipuladas. iJulienne está además dotada de un mecanismo de consulta de la traza que incrementa la flexibilidad y poder de reducción y permite examinar las ejecuciones de programas en el nivel apropiado de abstracción