Título: Bisimulación de Data-aware Communicating Finite State Machines con propiedades en las acciones
Directores: Carlos Gustavo Lopez Pombo, Hernán Melgratti
Jurados: Sergio Abriola, Emilio Tuosto

Resumen:
Los nuevos paradigmas de computación, como service-oriented computing (SOC) o
Cloud/Fog, como así también el Internet de las cosas (IoT por su sigla en
inglés), han impulsado enormemente lo que hoy se denomina economía de APIs. La
idea que subyace en la economía de APIs es la posibilidad de construir nuevos
servicios utilizando APIs provistas por terceras partes y, a su vez, hacer
disponibles estos nuevos servicios, publicando sus propias APIs. La creciente
interconexión entre aplicaciones y dispositivos hacen al surgimiento de nuevos
y esenciales requerimientos por parte de las aplicaciones actuales, tales como
self-adaptiveness y reconfiguración dinámica transparente. En la industria
actual, las APIs representan el último escalón de interoperabilidad, y ponen
en relieve la necesidad de descripciones precisas como forma preponderante de
documentación. Sin embargo, en la mayoría de los casos, los aspectos más
importantes del comportamiento de las API son documentados informalmente,
dificultando la validación del software que se obtiene como resultado de
componer servicios a través de sus APIs, así como el establecimiento de
propiedades y el mantenimiento de aplicaciones. En consecuencia, describir
formalmente el comportamiento de las APIs de forma que este provea garantías a
sus clientes constituye un desafío técnico clave en este contexto. El presente
proyecto de tesis asume una perspectiva en la que el ideal detrás de la
ejecución de aplicaciones basadas en APIs se lleva a cabo sobre una
infraestructura de comunicación y cómputo ubicua y preexistente y en la que un
middleware es capaz de solicitar a un service-broker la búsqueda de un
servicio al que, sujeto a una negociación de nivel servicios (SLA por su sigla
en inglés, Service Level Agreements), pueda vincularse en forma completamente
automática y transparente, para que colectivamente sea posible alcanzar cierto
objetivo de negocios. Es necesario contar con descriptores de protocolos
precisos a nivel de servicio, así como alguna definición de compliance que
permita establecer equivalencia entre dichos protocolos. Como candidatos
idóneos a estos, surgen las Asserted Communicating Finite State Machines
(a-CFSM), capaces de describir el intercambio de mensajes entre participante
(o servicios) y de establecer condiciones sobre las variables intercambiadas
en dichos mensajes (pre-condiciones sobre mensajes enviados y post-condiciones
sobre mensajes recibidos). Ligado a la necesidad de una definición de
compliance, surge como problema el hecho de que las partes involucradas en la
comunicación no necesariamente se conocen entre sí, por lo que descriptores
que resulten equivalentes pueden encontrarse escritos utilizando terminología
distinta. En este trabajo nos concentraremos en: 1) abordar una noción de
bisimulación a modo de compliance para las a-CFSM, asumiendo que los autómatas
comparten terminología, 2) extender la definición de bisimulación construyendo
un matching de nombres (un diccionario entre las terminologías de ambos
autómatas) y 3) poner en práctica los resultados obtenidos en (1) y (2) a
través de la construcción de una herramienta de software. Para facilitar (1),
definiremos una abstracción de las a-CFSM a las que llamaremos Assertable
Finite State Machines (a-FSM), con la que procederemos a definir tres nociones
de bisimulación de manera incremental (cada una a partir de las limitaciones
de la anterior), para posteriormente extender hacia las a-CFSM.