Implementación de un intérprete para un modelo concurrente para el análisis de sistemas síncronos

Abstract

[ES] Actualmente, el estudio del comportamiento concurrente de los sistemas es fundamental para poder disponer de herramientas que faciliten el análisis y verificaciones de programas con este tipo de comportamiento. Por ello, la existencia de lenguajes que modelan estos mecanismos concurrentes son de gran utilidad. El presente proyecto abarca el diseño e implementación de un intérprete que permite la ejecución de un modelo abstracto para lenguajes concurrentes síncronos. Se trata de un modelo síncrono que puede verse como un lenguaje intermedio al que se pueden traducir otros lenguajes concurrentes síncronos usados en la industria como pueden ser Promela, Esterel, Signal, etc. El intérprete desarrollado analiza un programa que siga la especificación semántica del modelo, ciñéndose al caso de los lenguajes imperativos, y simula su comportamiento. El resultado sirve de framework para la verificación formal de estos programas mediante el uso de técnicas preexistentes de análisis en tiempo de ejecución y permite su extensión para dar soporte a la simulación de programas aproximados por interpretación abstracta.

[CA] Actualment, l'estudi del comportament concurrent dels sistemes és fonamental per a poder disposar d'eines que faciliten l'anàlisi i verificacions de programes amb aquesta mena de comportament. Per això, l'existència de llenguatges que modelen aquests mecanismes concurrents són de gran utilitat. El present projecte abasta el disseny i implementació d'un intèrpret que permet l'execució d'un model abstracte per a llenguatges concurrents síncrons. Es tracta d'un model síncron que pot veure's com un llenguatge intermedi al qual es poden traduir altres llenguatges concurrents síncrons usats en la indústria com poden ser Promela, Esterel, Signal, etc. L'intèrpret desenvolupat analitza un programa que seguisca l'especificació semàntica del model, cenyint-se al cas dels llenguatges imperatius, i simula el seu comportament. El resultat serveix de framework per a la verificació formal d'aquests programes mitjançant l'ús de tècniques preexistents d'anàlisis en temps d'execució i permet la seua extensió per a donar suport a la simulació de programes aproximats per interpretació abstracta.

[EN] Currently, the study of the behavior of concurrent systems is essential to be able to have tools that facilitate the analysis and verification of programs with this kind of behavior. For this reason, the existence of languages that model these concurrent mechanisms are of great usefulness. The present project covers the design and implementation of an interpreter that allows the execution of an abstract model for synchronous concurrent languages. This synchronous model can be seen as an intermediate language to which other synchronous concurrent languages used in the industry can be translated to, such as Promela, Esterel, Signal, etc. The developed interpreter analyzes a program that follows the semantic specification of the model, sticking to the case of imperative languages, and simulates its behavior. The result serves as a framework for the formal verification of these programs by using preexisting techniques of analysis at runtime and allows its extension to support the simulation of approximate programs by abstract interpretation.