A Rewriting-based, Parameterized Exploration Scheme for the Dynamic Analysis of Complex Software Systems
Francisco Frechina Navarro · 2014
que permite la ejecución indeterminista de una teoría de reescritura condicional dada y que puede ser objeto de seguimiento mediante el uso de diferentes modalidades, incluyendo una ejecución gradual paso a paso y una fragmentación automática hacia adelante (y/o hacia atrás), lo que reduce drásticamente el tamaño y la complejidad de las trazas bajo inspección y permite a los usuarios evaluar de forma aislada los efectos de una declaración o instrucción dada, el seguimiento de los efectos del cambio de la entrada, y obtener información sobre el comportamiento del programa (o mala conducta del mismo).Por otra parte, la fragmentación de la traza de ejecución puede identificar nuevas oportunidades de optimización del programa.Con esta metodología, un analista puede navegar, fragmentar, filtrar o buscar en la traza durante la ejecución del programa.El marco de análisis de trazas genérico se ha implementado en el sistema Anima y describimos una profunda evaluación experimental del marco que demuestra la utilidad del enfoque propuesto. ResumEls sistemes programari de hui en dia són artefactes complexos el comportament dels quals és sovint extremadament difícil d'entendre.Este fet ha portat al desenrotllament de sofisticades metodologies formals per a l'anàlisi, comprensió i depuració de programes.L'anàlisi de traces d'execució consistix en tècniques que permeten buscar dinàmicament contingut específic en les traces d'execució d'un cert programa.La busca pot dur-se a terme cap avant o cap arrere.Si bé l'anàlisi cap avant es traduïx en una forma d'anàlisi sobre l'impacte que identifica l'abast i les possibles conseqüències dels canvis en l'entrada del programa, l'anàlisi cap arrere permet dur a terme l'anàlisi de la procedència; és a dir, mostra com (parts de) una eixida del programa depén de (parts de) la seua entrada i ajuda a estimar quines dades d'entrada són necessaris modificar per a dur a terme un canvi en el resultat.En esta tesi, s'investiga una sèrie de metodologies d'anàlisi de traces que són especialment adequats per a l'anàlisi de traces d'execució llargues i complexes en la lògica de reescriptura (RWL) , que és un marc lògic i semàntic especialment adequat per a la formalització de sistemes altament concurrents i complexos.La primera part de la tesi se centra a desenrotllar una tècnica (basada en la fragmentació incremental) d'anàlisi de traces cap arrere que aconseguix enormes reduccions en la grandària de la traça.Esta metodologia afavorix una millor anàlisi i depuració ja que la majoria de les inspeccions tedioses i irrellevants que es realitzen rutinàriament en el diagnòstic i la localització d'errors es poden eliminar de forma automàtica.Esta tècnica s'il•lustra per mitjà de diversos exemples que executem per mitjà del sistema iJulienne, una ferramenta interactiva de fragmentació que hem desenrotllat i que implementa la tècnica d'anàlisi de traces cap arrere.En la segona part de la tesi es formalitza un sistema paramètric, ric i molt dinàmic, per a l'exploració de computacions en lògica de reescriptura.L'esquema implementa un algoritme d'animació genèric que permet l'execució indeterminista d'una donada teoria de reescriptura xviii condicional que serà objecte de seguiment per mitjà de l'ús de diferents modalitats, incloent una execució gradual pas a pas i una fragmentació automàtic cap avant i cap arrere, la qual cosa reduïx dràsticament la grandària i la complexitat de les traces baix inspecció i permeten als usuaris avaluar els efectes d'una donada declaració o instrucció de forma aïllada, el seguiment dels efectes del canvi de l'entrada, i obtindre informació sobre el comportament del programa (o mala conducta).D'altra banda, la fragmentació de la traça d'execució pot exposar les oportunitats d'optimització del programa.Amb esta metodologia, un analista pot navegar, fragmentar, filtrar o buscar en la traça durant l'execució del programa.El marc d'anàlisi de traces genèrica s'ha implementat en el sistema Anima i una profunda avaluació experimental reporta la utilitat de l'enfocament proposat.1 Backward Trace Slicing for Conditional Rewrite Theories 1.1 Backward Slicing for Execution Traces . . . . . . . . . .1.2 The Function slice-step . . . . . . . . . . . .