Abstract
El entorno del trabajo se sitúa en la investigación de varios aspectos de la ingeniería del software, -entre otros, la modelización, especificación y validación -, además de la aplicación de tal ingeniería, al desarrollo de herramientas y técnicas para los protocolos de comunicación en el entorno de la Interconexión de Sistemas Abiertos (ISA). En el presente trabajo se introduce un modelo algebraico encaminado a la validación de la corrección de protocolos, que además unifica las consideraciones de rendimiento y prestaciones, a través de una semántica probabilista. Partiendo de tal modelo, se propone una metodología de diseño para facilitar el buen rendimiento de la validación de las especificaciones de protocolos y servicios, antes de la etapa de implementación. La propuesta de la metodología concreta, lleva asociado el desarrollo de herramientas apropiadas para la validación de especificaciones que, tomando como base el modelo propuesto, permiten el uso de diferentes lenguajes de especificación formal, cada uno posiblemente adecuado a la descripción de diferentes elementos de los sistemas distribuidos, y adaptados a la validación: Se toman como casos de estudio LOTOS y ESTELLE. ABSTRACT The objetives of the present work have been directed towards researching on several software engineering aspects, - i.e. modelling, specification and validation -, and also covering the application of such engineering to the development of techniques and tools for protocols in the Open Systems Interconnection (OSI) framework. In this work an algebraic model is introduced for the protocol correctness validation, unifying functional and performance aspects by means of a probabilistic semantic. Based on such a model, a dessign methodology is proposed for a good performance and easiness of protocol and service specifications validation, before the implementation stage. The proposed methodology is accomplished by the development of tools for proper specifications validation. Based on the proposed model, such kind of tools provide support to several formal specification languages, each of them possibly offering fitness to different distributed system components, and adequacy to validation: We have selected LOTOS and ESTELLE.
