Formalización y representación de especificaciones computacionales

Durante la ultima decada hemos asistido a una revolucion en cuanto a la normalizacion internacional en aspectos relacionados con las Tecnologias de la Informacion se refiere, Un ejemplo relevante es el caso de UML, que se ha convertido en el estandar mas utilizado como lenguaje de modelado de sistemas. Otro importante estandar es RM-ODP, cuya autoria corresponde a las organizaciones ISO/IEC e ITU-T, que plantearon a mediados de los 90 una serie de normas para el desarrollo de aplicaciones abiertas y distribuidas definiendo los conceptos, mecanismos y servicios apropiados. Este modelo de referencia proporciona una arquitectura basada en la separacion de conceptos mediante cinco puntos de vista diferenciados y la definicion de lenguajes abstractos para cada uno de ellos. Ademas, integra aquellos temas relacionados con la distribucion, interoperabilidad y portabilidad, asi como otros aspectos propios de estos sistemas: flexibilidad, calidad de servicio, modularidad, federacion, etc. La difusion y aceptacion de los estandares requiere no solo tiempo, sino tambien la disponibilidad de soportes y herramientas que faciliten su uso. Por ello, este trabajo de tesis propone una serie de notaciones concretas para la formalizacion y representacion del punto de vista computacional de RM-ODP, encargado de la especificacion funcional de los objetos computacionales, y de su interaccion a traves de interfaces, de un sistema abierto y distribuido. Cada una de estas notaciones esta orientada a un tipo especifico de usuario interesado en RM-ODP. Para ello, se propone Maude como formalismo, debido a su expresividad, alto rendimiento y capacidad de ejecucion, y UML 2 como representacion grafica, menos formal pero ampliamente extendida entre los ingenieros software. Finalmente, para reducir distancias entre estas notaciones, el desarrollo de software dirigido por modelos permite definir transformaciones automaticas entre ambos mundos, de modo que ingenieros no expertos en formalismos tomen tambien provecho, a partir de sus modelos UML, de las capacidades de verificacion de propiedades, comprobacion de modelos y simulacion y ejecucion temprana que proporciona Maude.