Mejorando un sistema de soporte para la calidad de software

Abstract

[ES] Este trabajo se enmarca dentro de un proyecto que tiene como objetivo el análisis y verificación de propiedades de sistemas concurrentes. De forma más precisa, en este TFG se desarrolla el módulo de la aplicación dedicada a la comprobación de satisfacibilidad de una fórmula LTL que se construye en los pasos anteriores del análisis. Dado que se parte de la salida de las fases anteriores de la aplicación TADi, con una sintaxis y estructura ya decididas se ha desarrollado un parser para satisfacer las necesidades del sistema. Así pues, en este trabajo se presenta el desarrollo de la aplicación basada en el algoritmo de validación de fórmulas LTL.

[EN] This work is part of a project that aims at analyzing and verifying properties of concurrent systems. More precisely, in this final degree application module dedicated to checking satisfiability of LTL formula that builds on the previous steps of the analysis is developed. Given that part of the output of the previous phases of the Tadi application with syntax and structure it has already decided parser developed to meet the needs of the system. So, in this work the development of the algorithm based on LTL formulas validation application is presented.