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

Sujets

• Lenguaje de programación

Informations

• Publié par: universidad_complutense_de_madrid
• Publié le: 01 janvier 2011
• Nombre de lectures: 45
• Langue: Español
• Poids de l'ouvrage: 7 Mo

Extrait

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 acaba