Aspectos formales de un modelo de ejecución orientada a servicios

Institución otorgante:

Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales

Fecha:

2018-07-30

Tipo de documento: 

info:eu-repo/semantics/doctoralThesis
 

Formato:

application/pdf

Idioma:

spa

Temas:

SOC - SOA - SEMANTICA FORMAL - COREOGRAFIAS - ORQUESTACION - METODOS FORMALES - SOC - SOA - FORMAL SEMANTICS - CHOREOGRAPHIES - ORCHESTRATION - FORMAL METHODS

Descripción:

El software distribuido que resulta de los nuevos paradigmas que están emergiendo, tales como el de computación orientada a servicios (SOC), computación en la nube e internet de las cosas, está transformando el mundo de los sistemas de software de modo de dar soporte a aplicaciones capaces de responder y adaptarse a los cambios en su entorno de ejecución, dando impulso a lo que se conoce como la economía de las APIs. La idea que subyace a la economía de las APIs es que es posible construir piezas de software a partir de componer servicios previamente registrados en repositorios y provistos por terceros. Esto promete una generación de aplicaciones ejecutando sobre recursos computacionales y una infraestructura de comunicación globalmente distribuidos que, en tiempo de ejecución son reconfiguradas dinámica y transparentemente mediante la intervención de un middleware dedicado. Esta reconfiguración está sujeta a la negociación de un acuerdo de nivel de servicio - SLA [25]. En este paradigma los servicios de software son accedidos a través de sus APIs. Muchos de los aspectos relacionados con la provisión de fundamentos formales y herramientas para dar soporte a estos nuevos paradigmos han sido resueltos en los últimos años [66], sin embargo algunos permanecen abiertos. En particular la habilidad para proveer una infraestructura capaz de llevar a cabo los procesos de discovery y bindig de manera completamente automática es aún un desafío abierto [33, 59]. En esta tesis contribuimos a este objetivo haciendo foco en dos aspectos del problema: (1) la provisión de elementos formales capaces de capturar las particularidades de estos paradigmas siendo la más relevante el hecho de que no es posible saber en tiempo de diseño qué servicio, si es que alguno, podrá satisfacer un determinado requerimiento y (2) la necesidad de ser capaces de determinar en tiempo de ejecución si existe un servicio particular, en un repositorio dado, capaz de satisfacer un determinado requerimiento. Como contribución al punto (1) proporcionamos una semántica operacional para las Asynchronous Relational Networks [24] que captura tanto las transiciones internas como las acciones de reconfiguración que ocurren durante la ejecución de un servicio. También extendimos esta semántica con la habilidad para capturar reconfiguraciones no incrementales con respecto a la estructura, de modo de dar soporte a la falta de confiabilidad derivada de la infraestructura de ejecución. Como contribución al punto (2) exploramos el uso de CFSMs [9] en nuestro modelo para expresar tanto requerimientos como contratos de provisión de servicio. De esta manera recurrimos al mecanismo dado en [38] para proveer un chequedo de interoperabilidad automático para servicios. También extendimos las CFSMs y las equipamos con datos y condiciones de tipo asunción/garantía en la forma de fórmulas de primer orden sobre esos datos. De este modo transformamos a las CFSMs en un mecanismo apropiado para expresar y chequear contratos funcionales restringidos.

Identificador:

https://hdl.handle.net/20.500.12110/tesis_n6483_Vissani