Una propuesta de formalización de la arquitectura en cuatro capas de UML

Resumen

Se presenta una propuesta de formalización de la arquitectura en cuatro capas de UML, destinada a representar, animar, validar, verificar y transformar formalmente modelos de sistemas de información construidos haciendo uso del lenguaje UML (Univied Modeling Language), El enfoque elegido ofrece un marco teórico para UML sin solución de continuidad, integral y evolutivo, obtenido como resultado de analizar tres posibles estrategias para formalizar un lenguaje de modelado. Tanto los aspectos de la sintaxis como la de la semántica de un subconjunto del diagrama de clases y del diagrama de estados de UML son descritos en un contexto algebraico, ofreciendo al usuario la posibilidad de establecer razonamientos y generar automáticamente prototipos de los mdoelos diseñados. Algunas propiedades de la semántica estática y de la semántica dinámica de UML, comola ortogonalidad de un diagrama de estados y la violación de la multiplicidad de un extremo de asociación, ilustran la verificación de propiedades en los modelos obtenidos. Asimismo, se explotan dos de las aplicaciones que mejor se adaptan a la estrategia y al lenguaje elegidos: la transformación de diagramas, ilustrada a través de la dedución de asociaciones derivadas en un diagrama de clases, y la extensión del propio lenguaje UML en tiempo de modelado. Maude, un lenguaje formal basado en lógica ecuacional y lógica de reescritura, ha sido adoptado para llevar a cabo los objetivos marcados. La reflexión, una propiedad demostrada en la lógica de reescritura e implementada eficientemente en el intérprete de Maude, juega un papel fundamental para que la evolución esté presente en las cuatro capas de la arquitectura de UML consideradas bajo el marco formal.