Coordinación de servicios Webde las aplicaciones a los modelos formales

Résumé

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.