Herramienta para automatizar la transformación UML/OCL a Object-Z

Abstract

En el proceso de construcción de software, el análisis y diseño son una tarea muy importante. UML (Unified Modeling Language, [OMG]) ha sido desarrollado para modelar sistemas Orientado a Objetos integrando lenguajes predecesores tales como la notación de Booch, OMT, etc. Este lenguaje ha sido aceptado como un estándar por OMG (Object Management Group) en el año 1997 [OMG]. Los principales diagramas provistos por UML son: diagramas de casos de usos, diagramas de clases, diagramas de estados, diagramas de secuencias. UML también provee un lenguaje textual, OCL (Object Constraint Language), fácil de leer y de escribir, que permite especificar características adicionales sobre los modelos en una forma similar a lógica de predicados. OCL es un lenguaje semi formal, su sintaxis está precisamente definida pero su semántica aún presenta ambigüedad, imprecisión e inconsistencia. Las expresiones OCL no tienen efectos laterales, es decir que su evaluación no puede alterar el estado del sistema correspondiente. Su evaluación solamente retorna un valor. En este trabajo presentamos una traducción de UML/OCL en lógica de predicados de primer orden. El objetivo es verificar propiedades de los diagramas UML y verificar la validez de las expresiones OCL que acompañan a dichos diagramas. Para ello se define una sintaxis y semántica para OCL. El beneficio de esta formalización es permitir la evaluación de expresiones OCL en un modelo UML.