Registro:
| Documento: | Tesis de Grado |
| Título: | Una noción de subtipado para asserted communicating finite state machines |
| Título alternativo: | A subtyping notion for asserted communicating finite state machines |
| Autor: | Monteys, Lautaro |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2025-01-01 |
| Fecha de defensa: | 2020 |
| Fecha en portada: | 2020 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | López Pombo, Carlos Gustavo |
| Jurado: | Melgratti, Hernán Claudio; Martínez Suñé, Agustín Eloy |
| Idioma: | Español |
| Palabras clave: | COMMUNICATING FINITE-STATE MACHINES; API; SUBTIPADOCOMMUNICATING FINITE-STATE MACHINES; API; SUBTYPING |
| Formato: | PDF |
| Handle: |
https://hdl.handle.net/20.500.12110/seminario_nCOM000864_Monteys |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000864_Monteys.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000864_Monteys |
| Ubicación: | COM 000864 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Monteys, Lautaro. (2020). Una noción de subtipado para asserted communicating finite state machines. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000864_Monteys |
Resumen:
Las últimas décadas han visto la explosión de servicios de Cloud computing a través del desarrollo y uso de APIs (Application Programming Interfaces) como método de interoperabilidad. Sin embargo, muchas veces estas APIs no se encuentran especificadas de manera precisa, lo que impide verificaciones formales sobre su comportamiento y dificulta la automatización de su uso. Esto genera grandes costos en desarrollo para aprovecharlas y las vuelve propensas a errores. Por lo tanto, describir formalmente el comportamiento de las APIs para proveer garantías es un desafío clave. El presente proyecto de tesis se construye sobre una infraestructura asumida preexistente con un repositorio de servicios donde un middleware puede colaborar con un service broker para encontrar y vincular servicios de forma automática y transparente. Se propone el uso de Communicating Finite State Machines (CFSMs) como candidatos idóneos para la descripción de protocolos. Los CFSMs son autómatas finitos, que representan a los participantes de la comunicación, cuyas transiciones están etiquetadas con envíos o recepciones de mensajes. En particular, se explora una nueva noción de subtipado que brinde un modelo de verificación más flexible dentro de esta infraestructura, relajando los requisitos estrictos de la bisimulación de participantes. El objetivo central es desarrollar una noción de subtipado para Asserted Communicating Finite State Machines (a-CFSMs). Las a-CFSMs extienden las CFSMs al permitir que las transiciones estén decoradas con aserciones (fórmulas en lógica de primer orden) que especifican restricciones sobre los datos intercambiados en los mensajes. En este trabajo definimos una relación de subtipado para CFSMs estándar, centrada en los aspectos estructurales de la comunicación. Luego, esta definición se extiende a las a-CFSMs y, finalmente, se demustra la correctitud de la extensión del subtipado a las a-CFSMs, preservando las propiedades de seguridad de la comunicación junto con de la flexibilidad agregada por el subtipado.
Abstract:
The last decades have seen the explosive growth of cloud computing services through the development and use of APIs (Application Programming Interfaces) as a means of interoperability. However, these APIs are often not specified precisely, which prevents formal verification of their behavior and hinders automation of their use. This imposes high development costs to leverage them and makes them error-prone. Therefore, the formal specification of API behavior, aimed at providing security guarantees, remains a key challenge. This thesis project is built on an assumed preexisting infrastructure consisting of a service repository in which a middleware can cooperate with a service broker to discover and bind services automatically and transparently. We propose the use of Communicating Finite State Machines (CFSMs) as suitable candidates for protocol specification. CFSMs are finite automata representing communication participants whose transitions are labelled with message sends or receives. In particular, we explore a new notion of subtyping that provides a more flexible verification model within this infrastructure by relaxing the strict requirements of participant bisimulation. The central objective is to develop a notion of subtyping for Asserted Communicating Finite State Machines (a-CFSMs). a-CFSMs extend CFSMs by allowing transitions to be decorated with assertions that specify constraints on the data exchanged in messages. In this work we define a subtyping relation for standard CFSMs focused on the structural aspects of communication. We then extend this definition to a-CFSMs and finally demonstrate the correctness of the extension for a-CFSMs, showing that it preserves the safety properties of communication while adding the flexibility provided by subtyping
Citación:
---------- APA ----------
Monteys, Lautaro. (2020). Una noción de subtipado para asserted communicating finite state machines. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000864_Monteys
---------- CHICAGO ----------
Monteys, Lautaro. "Una noción de subtipado para asserted communicating finite state machines". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2020.https://hdl.handle.net/20.500.12110/seminario_nCOM000864_Monteys
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000864_Monteys.pdf
Distrubución geográfica
