Depuración declarativa y verificación heterogénea en Maude = Declarative debugging and heterogeneous verification in Maude

UNIVERSIDAD COMPLUTENSE DE MADRID FACULTAD DE INFORMÁTICA Departamento de Sistemas Informáticos y Computación TESIS DOCTORAL Depuración declarativa y verificación heterogénea en Maude Declarative debugging and heterogeneous verification in Maude MEMORIA PARA OPTAR AL GRADO DE DOCTOR PRESENTADA POR Adrián Riesco Rodríguez Directores José Alberto Verdejo López Narciso Martí Oliert Madrid, 2011 ISBN: 978-84-695-1107-7 © Adrián Riesco Rodríguez, 2011 Depuraci´on Declarativa yVerificaci´on Heterog´enea en MaudeTESIS DOCTORALMemoria presentada para obtener el grado deDoctor en Inform´ aticaAdri´an Riesco Rodr´ıguezDirigida por los profesoresJos´e Alberto Verdejo L´opezNarciso Mart´ı OlietDepartamento de Sistemas Inform´aticos y Computaci´onFacultad de Inform´aticaUniversidad Complutense de MadridAbril 2011Declarative Debugging andHeterogeneous Verification in MaudePhD ThesisAdri´an Riesco Rodr´ıguezAdvisorsJos´e Alberto Verdejo L´opezNarciso Mart´ı OlietDepartamento de Sistemas Inform´aticos y Computaci´onFacultad de Inform´aticaUniversidad Complutense de MadridApril, 2011AcknowledgmentsI am finishing this PhD thesis being 28 years old.
Publicado el : sábado, 01 de enero de 2011
Lectura(s) : 45
Fuente : EPRINTS.UCM.ES/14454/1/T33189.PDF
Número de páginas: 394
Ver más Ver menos

UNIVERSIDAD COMPLUTENSE DE MADRID

FACULTAD DE INFORMÁTICA

Departamento de Sistemas Informáticos y Computación



TESIS DOCTORAL

Depuración declarativa y verificación heterogénea en
Maude

Declarative debugging and heterogeneous
verification in Maude


MEMORIA PARA OPTAR AL GRADO DE DOCTOR

PRESENTADA POR

Adrián Riesco Rodríguez


Directores

José Alberto Verdejo López
Narciso Martí Oliert

Madrid, 2011

ISBN: 978-84-695-1107-7

© Adrián Riesco Rodríguez, 2011 Depuraci´on Declarativa y
Verificaci´on Heterog´enea en Maude
TESIS DOCTORAL
Memoria presentada para obtener el grado de
Doctor en Inform´ atica
Adri´an Riesco Rodr´ıguez
Dirigida por los profesores
Jos´e Alberto Verdejo L´opez
Narciso Mart´ı Oliet
Departamento de Sistemas Inform´aticos y Computaci´on
Facultad de Inform´atica
Universidad Complutense de Madrid
Abril 2011Declarative Debugging and
Heterogeneous Verification in Maude
PhD Thesis
Adri´an Riesco Rodr´ıguez
Advisors
Jos´e Alberto Verdejo L´opez
Narciso Mart´ı Oliet
Departamento de Sistemas Inform´aticos y Computaci´on
Facultad de Inform´atica
Universidad Complutense de Madrid
April, 2011Acknowledgments
I am finishing this PhD thesis being 28 years old. Throughout these years I have met
several people that have been important for me and, since I believe that the decisions one
takes in his life are strongly influenced by the people surrounding him, I think that they
1are one of the main reasons I am here. Some of the people listed below could be added
in different categories; I have assigned them to the one I consider most fitting.
I would not be here without my parents, Gloria and Juan Julian,´ that have supported
me my whole life (literally). I also thank my sister Virginia, my uncles Antonio, Agust´ın,
Salva, Jul´ın, and Chete my aunts Encarna, Marlena, and Nena and my cousins Rosana,
Guillermo, Quique, and Marleni. I specially thank my grandparents Guadalupe, Mart´ın,
Juan Juli´an, and Loli, that cannot share this moment with us.
IstartedschoolwhenIwas2yearsold(IwasborninOctober),andIstayedinthesame
school—Nuestra Senor˜ a de las Delicias—until I was 16, so I was there for approximately
half my life thus far. I experienced in this period plenty of difficult situations but I
still remember lots of anecdotes, and it was there where I met some of my best (and of
course oldest) friends. First of all, I have to mention Charlie, with whom I have shared
uncountable hours in uncountable places and situations. In addition to him, I am also
happy to have shared my time with Remacha, Vincento, Pabl´e, Carro, Fran, Marisa,
Raquel, Lorena, and Paloma.
Being young and idealistic, some of the people listed above decided to create a football
team—Palacios A.D.—and see each other when we were not bound by school. We soon
realized that we were not enough to endure a whole match, much less to win it. Therefore,
we “bought” several players that have become our friends after 13 years of football and
“business meals,” with Polan, Pablo, Edu, Pesca, Juanito, and Miguelo being the most
important of them. As a matter of fact, we are still looking for a sponsor: do not hesitate
to contact me if you want to fund us.
IhavespentalotoftimeinAb´anades,asmallvillageinGuadalajara. There,Iampart
of a two-person guild with Jorge; when we are not playing videogames, running, eating
(we are specially proud of our torrijas), or reading, we interact with the rest of the world,
being the rest of the world in this case Mario, el Rober, Sonia, Alberto, Alfon, el Chini,
el Mun˜eco, and el Matis.
The most important person I met during my years at the university as an undergrad-
uate is Aida. She has always supported and helped me every time I have needed it, and I
must remark that our friendship survived even the construction of an AM transmitter in
LTC. During these years I can say that she has become part of my family, and I am sure
thatIoweseveralofmyvirtues(ifany), asengineerandasperson, toher. Asasideeffect,
I am also happy to have met her mother, Sole, who has taken care of me several times,
and her friend Maite. The second most important being that I met during these years is
la Pelotita. Although it is only a tennis ball, thanks to it a number of people, later known
1I just hope I would not be in a better place without them! ^¨
vvi
as The Buffer Crowd, was connected, and by playing with it the difficult moments were
easier. These players are Tom´as, DaGo, Javi, Fran, Edu, Adam, Luis, Lucas, Raul,´ and
Bea. I also want to thank two of my professors during this period: Joaqu´ın and Antonio.
Once I started my PhD studies, I saw the world from the dark side: the professors’
side. First of all I thank my advisors, Alberto and Narciso, and thank them for their
advice, their patience, their books, and their DVDs. I have very much enjoyed the lunches
with them and Ricardo, Miguel, Fernando, and Clara. I was also introduced to people
working around the world, and I want to highlight Santi, Salva, Paco, Gustavo, and Jos´e.
One year after starting my PhD studies I was assigned an office. There (here) I met
several people that make the daily life bearable, or even fun. They are Nacho, Enrique,
´Rober, Juan, dr. Alvez, Manu, Carlos, Quique Grande, and Dani. While working here I
have attended many conferences and schools, and I have got to meet very interesting and
kind people, that have both worked and partied with me. I would like to mention Mihai,
Till, Christian, Sebastian, Remy, Sasha, Dominik, Ewaryst, Berthold, and Kostas.
My research has been supported by the Ministerio de Educaci´on y Ciencia project
DESAFIOS (TIN2006-15660-C02-01), the Ministerio de Ciencia e Innovaci´on project DE-
SAFIOS10 (TIN2009-14599-C03-01), the Comunidad de Madrid projects PROMESAS
(S0505/TIC0407) and PROMETIDOS (S2009/TIC-1465), the Ministerio de Educaci´on y
Ciencia grants AP2005-007 and AP2005-0076.Agradecimientos
He acabado esta tesis doctoral con 28 an˜os. A lo largo de estos anos˜ he conocido
mucha gente que ha sido importante para mi y, dado que pienso que las decisiones que
uno toma en la vida se ven influenciadas por quienes le rodean, creo que ellos son unas de
2las principales razones por las que estoy hoy aqu´ı. Algunas de las personas enumeradas
a continuaci´on se podr´ıan haber an˜adido en diferentes categor´ıas; en estos casos, las he
situado en la que he considerado mas´ adecuada.
No estar´ıa aqu´ı sin mis padres, Gloria y Juan Juli´an, que me han apoyado toda mi
vida (literalmente). Tambi´en quiero mostrar mi agradecimiento a mi hermana Virginia,
mis t´ıos Antonio, Agust´ın, Encarna, Salva, Marlena, Nena, Jul´ın y Chete y mis primos
Rosana, Guillermo, Quique y Marleni. Dedico un agradecimiento especial a mis abuelos
Guadalupe, Mart´ın, Juan Juli´an y Loli, que no pueden compartir este momento conmigo.
Empec´eelcolegiocon2anos˜ (nac´ıenOctubre),yestuveenelmismocolegio—Nuestra
Senor˜ a de las Delicias—hasta los 16, lo que hace aproximadamente la mitad de mi vida.
Como en todos lados, tuve buenos y malos momentos, pero todav´ıa recuerdo con mucho
carin˜o esos d´ıas, y all´ı es donde conoc´ı a algunos de mis mejores (y obviamente m´as
antiguos) amigos. Dedico un agradecimiento especial a Charlie, con el que he pasado
innumerables momentos en los lugares y situaciones mas´ diversos. Adem´as, tambi´en me
alegra haber conocido a Remacha, Vincento, Pabl´e, Carro, Fran, Marisa, Raquel, Lorena
y Paloma.
Cuando eramos j´ovenes y entusiastas unos cuantos amigos decidimos crear un equipo
de fu´tbol—el Palacios A.D.—para seguir vi´endonos cuando dej´asemos de estudiar juntos.
Pronto nos dimos cuenta de que no eramos capaces de ganar un solo partido por nosotros
mismos, por lo que decidimos “fichar” a algunos jugadores que, despu´es de 13 an˜os de
fu´tbol y “concentraciones” han acabado siendo amigos, como Polan, Pablo, Edu, Pesca,
Juanito y Miguelo. Por cierto, seguimos buscando patrocinador: no dudes en contactar
conmigo si quieres serlo.
He pasado mucho tiempo en Ab´anades, un pequeno˜ pueblo de Guadalajara. All´ı soy
parte de una pena˜ de dos personas con Jorge; cuando no estamos jugando a la play,
corriendo, comiendo (estamos especialmente orgullosos de nuestras torrijas) o leyendo,
interactuamos con el resto del mundo, siendo en este caso el resto del mundo Mario, el
Rober, Sonia, Alberto, Alfon, el Chini, el Munec˜ o y el Matis.
La persona m´as importante que conoc´ı como estudiante de ingenier´ıa es Aida. Siempre
me ha apoyado y ayudado cuando lo he necesitado; baste decir como prueba de nuestra
amistad que superamos la construcci´on de un emisor de AM en LTC, lo cual incluye la
quema de transistores, que casi supone la p´erdida de nuestras huellas dactilares, y un
nocivo y gigantesco cristal de cuarzo. Durante estos anos˜ he acabado considerand´ ola parte
de la familia, y estoy seguro que muchas de mis virtudes (¡en el caso de tener alguna!),
comoingenieroycomopersona,selasdeboaella.Adem´as,conci´endolahetenidolasuerte
2¡Solo espero que sin ellos no estuviese hoy en un lugar mejor! ^¨
viiviii
de conocer a su madre, Sole, que siempre se ha preocupado por m´ı, y a su amiga Maite. El
segundo “ser” mas´ importante de los que conoc´ı en la facultad durante aquellos anos˜ es la
Pelotita. Aunque simplemente es una pelota de tenis, gracias a ella un grupo de personas,
m´as tarde conocidas como The Buffer Crowd, se conocieron, y jugando con ella se hicieron
m´as llevaderos los momentos complicados. Estos jugadores son Tom´as, DaGo, Javi, Fran,
Edu, Adam, Luis, Lucas, Raul´ y Bea. Por ul´ timo, tambi´en quiero nombrar aqu´ı a dos
profesores que conoc´ı durante este periodo: Joaqu´ın y Antonio.
Alempezareldoctorado,vielmundodesdeelladooscuro:elladodelosprofesores.En
primer lugar quiero agradecer a mis directores, Alberto y Narciso, sus consejos, paciencia,
libros y DVD. Tambi´en me lo he pasado muy bien comiendo con ellos y con Ricardo,
Miguel, Fernando y Clara. Adem´as, me han presentado a muchas otras personas como
Santi, Salva, Paco, Gustavo y Jos´e.
Un ano˜ despu´es de empezar el tercer ciclo me asignaron un despacho. All´ı (aqu´ı)
conoc´ı a muchas personas que hacen que la vida diaria sea divertida. Ellos son Nacho, En-
´rique, Rober, Juan, dr. Alvez, Manu, Carlos, Quique Grande y Dani. Adem´as, trabajando
aqu´ı he asistido a varias conferencias y escuelas y he conocido a mucha gente, con la que
he trabajado y salido de fiesta. Me gustar´ıa resaltar a Mihai, Till, Christian, Sebastian,
Remy, Sasha, Dominik, Ewaryst, Berthold, and Kostas.
Poru´ltimo,miinvestigaci´onhasidofinanciadaporelproyectodelMinisteriodeEduca-
ci´on yCiencia DESAFIOS (TIN2006-15660-C02-01), el proyecto delMinisterio de Ciencia
e Innovaci´on DESAFIOS10 (TIN2009-14599-C03-01), los proyectos de la Comunidad de
Madrid PROMESAS (S0505/TIC0407) y PROMETIDOS (S2009/TIC-1465), y las becas
del Ministerio de Educaci´on y Ciencia AP2005-007 y AP2005-0076.ix
Abstract
Declarative debugging is a semi-automatic technique that starts from an incorrect
computationandlocatesaprogramfragmentresponsiblefortheerror. Wecandistinguish
two phases in this scheme: in the first one the computation is represented as a debugging
tree, while in the second one the debugger traverses this tree until the error is found
by asking questions related to the adequacy of the judgments stored in the nodes to an
externaloracle,usuallytheuser,followinganavigationstrategy. Thisdebuggingtechnique
can be used to debug two different kinds of errors: wrong answers, that is applied when
an erroneous result is obtained from an initial value, and missing answers, applied when
a result is incomplete.
The first part of this thesis applies these ideas to build a declarative debugger for
rewriting logic specifications in Maude. It shows how we have adapted the standard
calculus of rewriting logic to debug wrong answers, while we debug missing answers with
a new calculus that extends the one for wrong answers with judgments to infer, given
a term, its normal form, its least sort, and the set of reachable terms given a pattern,
a condition, and a bound in the number of steps. With this calculus we can detect
errors due to wrong and missing statements (equation, membership axioms, and rules)
and to wrong search conditions. We have proved that this technique is sound (the error
attributed by the debugger is in fact an error) and complete (we can always find the error)
ifsomerequirementsarefulfilled,namelythespecificationbeingdebuggedisanexecutable
Maude module and the information introduced by the user is correct. Finally, the use of
the debugger has been illustrated with several examples.
Formal systems like Maude provide several mechanisms to perform different analyses,
but it is unlikely that a single system will ever supply tools for every possible analysis a
programmer could require. Moreover, it is natural, when facing large systems, to specify
differentpartsindifferentways. Forthesereasonheterogeneousspecifications,whichallow
the programmer to use different formalisms, are becoming more and more important,
especially in safety-critical areas where one cannot take the risk of malfunction. One
of such systems is the Heterogeneous Tool Set (Hets), a formal integration tool that
provides parsing, static analysis, and proof management for heterogeneous specifications
by combining several individual specifications languages.
The second part of this thesis describes how to integrate Maude into Hets, in such
a way that the tools already integrated in the system can be used to analyze Maude
specifications. To achieve it we had to (i) define an institution for Maude, so thee
logiccanbeintegratedintoHets, (ii)defineacomorphismfromthisinstitutiontotheone
of Casl, the central logic of Hets, which combines higher-order logic and induction and
that has defined comorphisms to the rest of logic integrated in the system, which allows
to translate Maude to these logics, and (iii) translate Maude’s structuring mechanisms
to development graphs, the method used by Hets to represent structured specifications
and ease proof management. In our case, Maude modules and theories are represented as
nodes, importations as edges, and views as edges with associated proof obligations.

¡Sé el primero en escribir un comentario!

13/1000 caracteres como máximo.