La evolución de los sistemas de software y la creciente complejidad de sus procesos de desarrollo han hecho necesario establecer pasos de diseño bien definidos que permitan reducir el gap entre requerimientos e implementaciones. En esta dirección, en años recientes, un área importante de la investigación ha tratado con las Arquitecturas de Software. Básicamente, una arquitectura de software es una descripción de alto nivel de un sistema complejo, con un nivel adecuado de abstracción que permite capturar del dominio del problema los componentes, a partir de los requerimientos, que serán diseñados detalladamente más adelante. Un Estilo de Arquitectura de Software es una clase de arquitecturas que exhiben un patrón común. Si la reusabilidad y la clasificación de arquitecturas son objetivos principales para permitir que los diseñadores exploten el trabajo previo, la identificación de una arquitectura de un sistema dentro de un estilo específico requiere lenguajes expresivos y bien fundados para representar estilos. Los requerimientos de los sistemas modernos imponen nuevas características a la descripción de las arquitecturas de software. Estos incluyen la distribución, la concurrencia, la reconfiguración y la movilidad. Por lo tanto, es necesario desarrollar el lenguaje de estilos que soporte estas características y por consiguiente su semántica formal. Entonces, la descripción de un estilo de arquitectura de software debe incluir la estructura de los tipos de componentes y sus interacciones, los patrones de comunicación, y las leyes que gobiernan la reconfiguración y/o la movilidad en la arquitectura. Siguiendo esta línea de investigación, es nuestro objetivo contribuir a la formalización de modelos para la descripción de arquitecturas y estilos de arquitectura de software. Esta tesis presenta un marco formal para la descripción de estilos de arquitectura de software basado en los sistemas de transformación de grafos. Una gramática de grafos caracteriza una clase de grafos que comparten características estructurales y está compuesta por un conjunto de reglas de reescritura llamadas producciones. Inicialmente, los grafos representan las configuraciones estáticas de las arquitecturas y las gramáticas representan los estilos. Luego, podremos incluir producciones que especifiquen las interacciones en mntime entre componentes, la reconfiguración y la movilidad. Las arquitecturas de sistemas pueden ser controladas de manera centralizada a través de un coordinador o administrador, o pueden ser sistemas denominados self organising en los cuales la coordinación está distribuida localmente entre los componentes. Los sistemas que tenemos en mente son distribuidos, lieterogéneos y móviles, y por lo tanto elegimos una estrategia self organising. En particular, para describir estilos elegimos utilizar gramáticas libres de contexto para Recscritura de Hiperejes (Hyperedge Replacement (HR) granunars) y gramaticas HR de Sincronización (Synchronized HR (SHR) grammars) para modelar la comunicación y la coordinación entre componentes. Un hipereje es un elemento atómico con una etiqueta (de un alfabeto con rango) y con tantos tentáculos como el rango de su etiqueta. Un conjunto de nodos y un conjunto de liiperejes forman un hipergrafo si cada lripereje esta conectado, por sus tentáculos, con sus nodos de enlace (attachmcnt nodos). Los Hiperejes corresponden a los componentes y sus nodos de enlace son sus puertos de conmnicación con otros componentes. Una producción HR reescribe un solo hipereje en un hipergrafo cualquiera. Entonces, para modelar la coordinación de los componentes de la arquitectura combinamos reescritura de grafos con condiciones de sincronización, obteniendo los sistemas SHR. Las producciones sincronizadas se especifican agregando condiciones en los nodos que permiten coordinar varias reescrituras, determinando la manera en que los componentes interactúan y se reconfiguran. Las producciones para (la etiqueta de) un hipereje determinado representan las posibles evoluciones para un determinado tipo de componente del estilo. Las producciones de una gramática se agrupan en tres conjuntos: el primer conjunto contiene las producciones HR para la construcción de todas las posibles configuraciones iniciales del estilo. El segundo conjunto contiene las producciones SHR que modelan la evolución de la comunicación para cada tipo de componente, y el tercer conjunto contiene las producciones SHR para la reconfiguración de la estructura del estilo. Las producciones de la comunicación requieren sincronización pero no pueden cambiar la estructura topológica del grafo. Con respecto a literatura anterior. esta tesis presenta una extensión de los sistemas SHR con la adición de movilidad de nombres (name mobility como en π-calculus). Esta extensión permite aumentar substancialmente el poder expresivo del método para la representación de sistemas complejos móviles y reconfigurables, mantieniendo al mismo tiempo la capacidad de describirlos de una manera descentralizada y distribuida. Representamos a los liipergrafos y los sistemas SHR en forma textual usando syntactic judgements. Esto permite una clara separación entre reescritura y coordinación, y la introducción de varios mecanismos de sincronización como adecuadas álgebras (móviles) de sincronización. Específicamente, presentamos las reglas de inferencia al estilo SOS para las álgebras de sincronización Hoare (CSP) y Milner (CCS, π-calculus). Sin embargo. en nuestra propuesta extendemos las álgebras de proceso permitiendo la sincronización simultánea de cualquier número de participantes. Las condiciones de sincronización para movilidad se resuelven vía unificación. Como resultado importante y evidencia formal del poder expresivo del método, presentamos un resultado de correspondencia que prueba que SHR con sincronización de Milner subsume al π-calculus. Para esto, definimos una traducción donde una transición en π-calculus se representa como una transición del correspondiente syntactic judgement traducido (es decir, un paso de reescritura). Puesto que π-calculus está equipado con una semántica interleaving y sólo sincronizaciones entre pares de elementos, la prueba es una correspondencia completa entre π-calculus y una versión restringida de los sistemas SHR. En la segunda parte de la tesis continuamos usando gramáticas HR (sin sincronización) para describir estilos e introducimos un enfoque específico basado en teoría de tipos para describir las reconfiguraciones de estilos (llamadas transformaciones). Las nociones de reconfiguración y movilidad implican modificaciones a la estructura de la arquitectura cambiando componentes y conexiones. Estas modificaciones que un sistema puede sufrir conducen a la pregunta de cómo podemos asegurar que los cambios sean consistentes con el estilo al cual pertenece el sistema. Por analogía, podemos pensar en los estilos como tipos para las instancias de arquitectura y en derivaciones HR como pruebas de tipo. Las reconfiguraciones deben preservar los tipos: en terminología de la teoría de tipos esta propiedad se llama subject reduction. Nuestro método consiste en definir transformaciones sobre pruebas de tipo, en lugar que sobre grafos: mientras que cortar y pegar pruebas de tipo resulten nuevamente en pruebas de tipo, la propiedad de subjet reduction está garantizada. La formalización se efectúa representando grafos y producciones como términos de un cálculo λ tipado, donde un paso de derivación HR corresponde a aplicación seguido por reducción β. Entonces, las transformaciones se especifican como reescritura de términos (de alto orden): si todas las reglas de reescritura transforman pruebas de tipo en pruebas de tipo, entonces todas las posibles reescrituras satisfacen subject reduction. El uso de cálculo λ introduce la idea de reescritura de grafos de alto orden, permitiendo la parametrización del proceso de diseño con características de componentes y conectores que podrían ser especificados más adelante, manteniendo la garantía de consistencia. La principal diferencia del método para reconfiguración usando SHR con respecto al que utiliza transformaciones, es que SHR es más dinámico, ya que es aplicable a sistemas abiertos en ejecución sin control global, a excepción de la sincronización. Por el otro lado, el método con transformaciones puede ser útil para trabajar al nivel de diseño estático, es decir, cambiar los pasos del diseño del sistema para producir un sistema diverso pero consistente. De todas maneras, el último método puede ser aplicado para especificar clases muy generales de reconfiguraciones y movilidad (como se demuestra en los ejemplos de la tesis), pero requiere un conocimiento global de la estructura del sistema. Los diferentes temas introducidos en la tesis son acompañados por ejemplos específicos que permiten clarificar las diversas construcciones y demostrar su poder expresivo, y por un caso de estudio de un sistema remoto de asistencia médica que es utilizado a lo largo de toda la tesis.