Selección de un método formal de especificación como herramienta de diseño de un sistema distribuido basado en objetos.

Abstract

El problema de desarrollar un sistema de soporte para la interacción de objetos en la programación de sistemas distribuidos basado en objetos es complejo, por lo cual se requiere utilizar una herramienta que permita trabajar con un alto nivel de abstracción y verificar la correctitud del diseño y su realización. Con este fin se plantea como objetivo de este trabajo escoger un método de especificación formal, lo que se realiza en dos etapas: La primera identifica, utilizando un enfoque basado en el análisis de la bibliografía y de las publicaciones de experiencias realizadas, las características y propiedades tanto de los sistemas a especificar, como de diversos métodos formales, a fin de determinar a un nivel teórico cuáles de estos últimos permiten representaciones correctas de las primeras. Los métodos que resultan seleccionados en esta etapa son dos: Lógica Temporal de Acciones (TLA) y Cálculo de Sistemas de Comunicación con su extensión Abacus (CCS/Abacus). La segunda etapa consiste en desarrollar especificaciones de un sistema que posee las características identificadas previamente, en este caso una versión simplificada del sistema de correo electrónico Grapevine, mediante los métodos seleccionados en la etapa anterior, a fin de verificar en forma práctica cuál de ellos es el más adecuado para el propósito indicado, resultando seleccionado definitivamente CCS/Abacus, y además se obtiene experiencia para desarrollar este tipo de especificaciones; con ello se alcanza el objetivo planteado inicialmente. Como resultado adicional se obtiene algunas conclusiones acerca de la complejidad que presenta la aplicación de los métodos formales y las situaciones en que es conveniente utilizarlos.