Formalizing and Validating UML Architecture Description of Web Systems

Claramente es una extensión del trabajo anteriormente mostrado. Bajo el concepto de SO-SAM, esta vez Fu et al. [1] muestran cómo a partir de diagramas de estados y diagramas de secuencias modelados en UML, generan RdP y fórmulas de lógica temporal respectivamente.

Para cada uno de los diagramas involucrados, es decir, diagramas de estado y diagramas de secuencia, proponen reglas para sus respectivas transformaciones a RdP y fórmulas de lógica temporal. No obstante, señalan la inherente imposibilidad de probar la correctitud de las transformaciones, sin embargo, validan cuidadosamente la completitud y consistencia de sus reglas de transformación.

Para demostrar su propuesta proponen un caso de estudio que consiste en el procesamiento de imágenes usadas en aplicaciones Web distribuidas. La validación de su técnica se encuentra implícitamente en los métodos formales utilizados (RdP y lógica temporal) y desarrollan su propuesta a través del lenguaje Maude [2].

De acuerdo con los autores, los resultados presentados, muestran que es posible verificar propiedades estructurales y de comportamiento de los sistemas. Finalmente concluyen que su técnica combina los beneficios de UML (fácil de entender y numerosas herramientas de soporte) y la fácil manera de análisis de SO-SAM. Indican además, que el costo de su propuesta se centra en básicamente tres partes: la construcción de especificaciones algebraicas, la generación de redes de alto nivel a partir de los diagramas de estado y la creación de fórmulas basadas en lógica temporal a partir de los diagramas de secuencia.

Referencias

[1] Y. Fu, Z. Dong y X. He. Formalizing and Validating UML Architecture Description of Web Systems. ICWE’06 Workshops, July 1014, 2006, Palo Alto, California, USA. ACM 1595934359/06/07.

[2] Department of Computer Science, University of Illinois at Urbana-Champaign. The Maude System.
http://maude.cs.uiuc.edu/