Una herramienta para verificación formal de especificaciones gráficas orientadas a objetos

Abstract

Una de las claves para el éxito de la formalización propuesta reside en ocultar la notación matemática tanto como sea posible tras la notación gráfica. Por ejemplo, debería ser posible utilizar la semántica formal para desarrollar herramientas CASE. Sólo los desarrolladores deberían usar el formalismo del lenguaje para construir las herramientas CASE y justificar su corrección, mientras que los desarrolladores de software de aplicación podrían manejar los modelos gráficos sin necesidad de conocer el formalismo matemático subyacente. El objetivo de esta tesis es implementar una herramienta que permita el manejo del modelo conceptual propuesto. Dicha herramienta implementará un método de transformación automático, consistente en un conjunto de reglas para crear un modelo formal a partir de los modelos expresados en UML. La herramienta permitirá además el manejo del modelo formal, la aplicación de mecanismos de chequeo y la evolución en los distintos niveles de modelado. UML es parcialmente soportado por una herramienta CASE desarrollada por Rational Software Corporation, llamada Rational Rose. Esta aplicación permite crear especificaciones gráficas en UML, y generar un archivo con la representación textual de la especificación. La representación textual permite la manipulación de la especificación para diversos usos. Se espera que la nueva herramienta pueda integrarse dentro de la herramienta CASE de Rational Rose.