{\rtf1\ansi\ansicpg1252\cocoartf1038\cocoasubrtf350
{\fonttbl\f0\fswiss\fcharset0 Helvetica;}
{\colortbl;\red255\green255\blue255;}
\paperw11900\paperh16840\margl1440\margr1440\vieww9000\viewh8400\viewkind0
\pard\tx566\tx1133\tx1700\tx2267\tx2834\tx3401\tx3968\tx4535\tx5102\tx5669\tx6236\tx6803\ql\qnatural\pardirnatural

\f0\fs24 \cf0 Desde los or\'edgenes del hardware y el software hasta la \'e9poca actual, la complejidad de los sistemas de c\'e1lculo ha supuesto un problema al cual inform\'e1ticos, ingenieros y programadores han tenido que enfrentarse. Como resultado de este esfuerzo han surgido y madurado importantes \'e1reas de investigaci\'f3n. En esta disertaci\'f3n abordamos algunas de las l\'edneas de investigaci\'f3n actuales relacionada con el an\'e1lisis y la verificaci\'f3n de sistemas de computaci\'f3n complejos utilizando m\'e9todos formales y lenguajes de dominio espec\'edfico.\
\
En esta tesis nos centramos en los sistemas distribuidos, con un especial inter\'e9s por los sistemas Web y los sistemas biol\'f3gicos. La primera parte de la tesis est\'e1 dedicada a aspectos de seguridad y t\'e9cnicas relacionadas, concretamente la certificaci\'f3n del software. En primer lugar estudiamos sistemas de control de acceso a recursos y proponemos un lenguaje para especificar pol\'edticas de control de acceso que est\'e1n fuertemente asociadas a bases de conocimiento y que proporcionan una descripci\'f3n sensible a la sem\'e1ntica de los recursos o elementos a los que se accede. Tambi\'e9n hemos desarrollado un marco novedoso de trabajo para la Code-Carrying Theory, una metodolog\'eda para la certificaci\'f3n del software cuyo objetivo es asegurar el env\'edo seguro de c\'f3digo en un entorno distribuido. Nuestro marco de trabajo est\'e1 basado en un sistema de transformaci\'f3n de teor\'edas de reescritura mediante operaciones de plegado/desplegado. La segunda parte de esta tesis se concentra en el an\'e1lisis y la verificaci\'f3n de sistemas Web y sistemas biol\'f3gicos. Proponemos un lenguaje para el filtrado de informaci\'f3n que permite la recuperaci\'f3n de informaciones en grandes almacenes de datos. Dicho lenguaje utiliza informaci\'f3n sem\'e1ntica obtenida a partir de ontolog\'edas remotas para refinar el proceso de filtrado. Tambi\'e9n estudiamos m\'e9todos de validaci\'f3n para comprobar la consistencia de contenidos web con respecto a propiedades sint\'e1cticas y sem\'e1nticas. Otra de nuestras contribuciones es la propuesta de un lenguaje que permite definir y comprobar autom\'e1ticamente restricciones sem\'e1nticas y sint\'e1cticas en el contenido est\'e1tico de un sistema Web. Finalmente, tambi\'e9n consideramos los sistemas biol\'f3gicos y nos centramos en un formalismo basado en l\'f3gica de reescritura para el modelado y el an\'e1lisis de aspectos cuantitativos de los procesos biol\'f3gicos.\
\
Para evaluar la efectividad de todas las metodolog\'edas propuestas, hemos prestado especial atenci\'f3n al desarrollo de prototipos que se han implementado utilizando lenguajes basados en reglas.}