Resumen de Coordinación de servicios Web: de las aplicaciones a los modelos formales
- español
El objetivo de la tesis ha sido la aplicación de métodos formales en ingeniería del software con el fin de incrementar la fiabilidad de sistemas de software reales. En particular, se ha analizado un Servicio de Coordinación Web que forma parte de varias aplicaciones distribuidas, actualmente en explotación, en el contexto de los Servicios Basados en la Localización. El servicio de coordinación está construido sobre JavaSpaces (un implementación del modelo de coordinación Linda) y proporciona servicios para comunicar y sincronizar aplicaciones heterogéneas distribuidas en Internet.
Partiendo del sistema real, se ha obtenido un modelo formal con el fin de estudiar sus propiedades y se ha demostrado que el proceso de correspondencia implementado en el servicio respeta la semántica de Linda, además de posibilitar otros emparejamientos más complejos. Después se ha extendido el modelo Linda definiendo nuevas operaciones que involucran a varias tuplas y que lo dotan de capacidades transaccionales. Finalmente se ha realizado un análisis "semi-formal" de un algoritmo basado en RETE para la operación de lectura múltiple.
- English
The goal of the thesis was the application of formal methods in software engineering in order to increase the reliability of real software systems. In particular, a Web Coordination Service has been analyzed. This service is a component in several working distributed systems in the context of Location Based Services. The coordination service is based on JavaSpaces (an implementation of the Linda coordination model) and provides a set of services to communicate and synchronize heterogeneous applications distributed over the Internet.
Given a real-life system, a formal model was been obtained in order to study its properties and prove that the pattern-matching process implemented in the coordination service complies with the semantics rules of Linda. Moreover, the service enables other more complex matching processes. Then, the Linda model has been extended with operations where multiple tuples are involved. These new operations supply some transactional capabilities to the coordination model. Finally, a "semi-formal" analysis of a RETE-based algorithm for the multiple reading operation was performed.
