Comprobación de modelos en sistemas concurrentes a partir de su semántica en Maude

Abstract

La comprobación de modelos (model checking) es una técnica automática para verificar si una propiedad se cumple en un sistema concurrente. Maude es un marco lógico de alto rendimiento donde se puede especificar, modelar, ejecutar y analizar —de forma sencilla— otros sistemas. Además, este entorno incluye un comprobador de modelos para verificar propiedades expresadas en lógica temporal lineal. Sin embargo, cuando una propiedad aplicada a un programa —escrito en un lenguaje de programación modelado para Maude— no se cumple, el contraejemplo —generado por el propio sistema— está basado en la semántica del propio Maude, dificultando la tarea de poder seguirlo a la hora de entender el resultado. En esta memoria presentamos la herramienta Selene, un marco genérico que maneja sistemas concurrentes asíncronos de modo que el usuario pueda obtener una versión simplificada de los contraejemplos generados por el comprobador de modelos en Maude tras la realización del análisis sobre programas escritos en otros lenguajes. Para lograrlo se ofrece un kernel para manejar la memoria y los mensajes, elementos que se emplearán en el “informe” final obtenido del contraejemplo. Sobre dicha arquitectura el usuario podrá especificar los detalles de la semántica del lenguaje a manejar. Por último, se analizará cuáles fueron los objetivos iniciales, los resultados obtenidos, los problemas encontrados durante el desarrollo, así como las propuestas y líneas futuras de trabajo que serían deseables para la mejora del proyecto.

Model checking is an automatic technique for verifying whether some properties hold in a concurrent system. Maude is a high-performance logical framework where other systems can be easily specified, executed, and analyzed. Moreover, Maude includes a model checker for checking properties expressed in Linear Temporal Logic. However, when a property on a program written in a programming language specified in Maude does not hold the counterexample generated by this system refers to the Maude semantics, which might be difficult to follow. In this Master’s Thesis we present Selene, a generic framework for dealing with asynchronous concurrent systems that allows users to receive a simplified version of the counterexample generated by the Maude model checker to relate it to the program being analyzed. This is achieved by providing a kernel for dealing with messages and memory, which are later handled in the counterexample; the user can specify the details of his semantics on top of this kernel. Finally, it will be analyzed which were the initial objectives, the final results, the problems found in the development, as well as the proposals and future lines of work in the project to improve it.