Red2.pdf

´ UNIVERSIDAD POLITECNICA DE VALENCIA ´ ´ departamento de sistemas informaticos y computacion

tesis doctoral

Redes Reconfigurables. ´ ´ Modelizacion y Verificacion

Presentada por: Ma Luisa Llorens Agost Dirigida por: Dr. Javier Oliver Villarroya Valencia, 2003

A mi abuela. A mis padres. A mi hermano.

iii

Agradecimientos
Esta tesis ha sido el fruto de a˜os de trabajo. Nohubiera sido posible sin n la ayuda de mi familia, amigos y compa˜eros. Por ello, quiero dar las gracias: n A mi director de Tesis, Javier Oliver, que fue quien me anim´ a comenzar o los estudios de doctorado y quien ha hecho posible con su inter´s, su dedicaci´n e o y su paciencia que esta tesis saliera adelante. A mis compa˜eros del DSIC. En particular a Inma, por ser m´s que una n a n ocompa˜era, por ser mi amiga. Y a Gabi, por apoyarme y por darme la soluci´n a tantos problemas que, para m´ parec´ no tenerla. ı, ıan A mi familia, por estar siempre a mi lado, d´ndome su cari˜o, su apoyo a n y su comprensi´n. En especial a mis padres y a mi hermano, porque siempre o han estado ah´ cuando los he necesitado. ı e A mis amigos de siempre. Especialmente a Bea y a Lourdes, porque s´ quesiempre podr´ contar con ellas. e A todos... gracias.

v

Resumen
En esta Tesis Doctoral se aborda el problema de la modelizaci´n y la verio ficaci´n de sistemas concurrentes sujetos a cambios din´micos. El formalismo o a de base es el de las redes de Petri. En lo que concierne a la expresividad del modelo se busca un mecanismo que tenga en cuenta los cambios din´micos a estructurales de maneralocal, interna e incremental. Al mismo tiempo, las propiedades b´sicas de las redes de Petri (acotabilidad de lugares, alcanzabia lidad, interbloqueo y vivacidad) deben continuar siendo decidibles para este modelo extendido. En general, lo que se gana normalmente en t´rminos de e expresividad se traduce en una p´rdida en t´rminos de propiedades decidibles. e e Hay que buscar, entonces, unequilibrio entre expresividad y computabilidad. Las gram´ticas de grafos y las redes automodificantes de Valk son las dos a ıneas de investigaci´n origen de nuestro modelo general: los sistemas de reeso l´ critura de redes. Ambas l´ ıneas dan lugar a modelos que mejoran la expresividad a de las redes de Petri para describir el cambio din´mico en sistemas concurrentes pero tienen el inconveniente de quecasi todas las propiedades b´sicas decidia bles de las redes de Petri se pierden. Por ello, para estos modelos extendidos no pueden construirse herramientas autom´ticas de verificaci´n. a o Los sistemas de reescritura de redes son una combinaci´n de redes de Petri o con sistemas de reescritura de grafos. Cada configuraci´n del sistema es una o red de Petri y un cambio de configuraci´n es una regla dereescritura de grafos. o La expresividad de los sistemas de reescritura de redes es la misma que la de la m´quina de Turing, es decir, las propiedades b´sicas decidibles de las redes de a a Petri se pierden en estos sistemas, no siendo posible la verificaci´n autom´tica. o a Las redes reconfigurables son una subclase de los sistemas de reescritura de redes equivalente formalmente a las redes dePetri, lo que asegura que todas las propiedades fundamentales de las redes de Petri siguen siendo decibibles para este modelo y, por tanto, es factible la verificaci´n autom´tica. o a

vii

Resum
En aquesta Tesi Doctoral s’ aborda el problema de la modelitzaci´ i la verio ficaci´ de sistemes concurrents subjectes a canvis din`mics. El formalisme de o a base ´s el de les xarxes de Petri. Pel quefa a l’ expressivitat del model es busca e un mecanisme que tinga en compte els canvis din`mics estructurals de manera a local, interna i incremental. Al mateix temps, les propietats b`siques de les a xarxes de Petri (acotabilitat de llocs, assequibilitat, interbloqueig i vivacitat) deuen continuar sent decidibles per aquest model est`s. En general, el que es e guanya normalment en termes d’...