Abstract:
El diseño, especificación, validación y construcción de sistemas distribuidos representa un reto de complejidad elevada tanto desde el punto de vista matemático como de ingeniería. Aunando a esto, el impacto que tienen estos sistemas, tanto en la industria como en la vida diaria, los hace una de las líneas de investigación y desarrollo más activas e interesantes dentro de las ciencias de la computación.
En la presente tesis, se desarrolla un lenguaje gráfico de especificación, un álgebra de procesos, un algoritmo de transformación y una herramienta matemática que en conjunto forman un marco de trabajo para la especificación y validación de sistemas distribuidos. El lenguaje de especificación, llamado Lenguaje Gráfico de Especificación de Sistemas Distribuido (LeGESD), está basado en una sintaxis gráfica, la cual permite construir elementos sintácticos gráficos mediante el seguimiento de reglas sintácticas claramente establecidas. El algoritmo de transformación está sustentado por un conjunto de teoremas de transformación que permiten transformar la especificación de un sistema distribuido realizada en el lenguaje gráfico a una especificación equivalente en un álgebra de procesos llamada Análisis y Diseño de Sistemas Distribuidos (ADSD).
La herramienta matemática está compuesta del teorema de equivalencia gráfico-algebraica y de una serie de teoremas que establecen la equivalencia entre la especificación gráfica y la especificación algebraica obtenida a partir de ejecutar el algoritmo de transformación sobre dicha especificación gráfica. El resultado principal de la herramienta es establecer que las validaciones de propiedades de seguridad demostradas en la especificación algebraica son igualmente válidas para la especificación gráfica, y viceversa.
Finalmente, se desarrollan dos ejemplos que muestran la utilización tanto del lenguaje como de su semántica asociada, una vez que esta ´ultima es obtenida a partir de la ejecución del algoritmo de transformación.
