Generación de monitores C embebidos para especificaciones Lola

En las últimas décadas se ha experimentado un gran crecimiento en el desarrollo de sistemas embebidos para diversas áreas de aplicación, muchas de las cuales involucran sistemas críticos donde resulta imprescindible proveer garantías de correctitud. Las técnicas de verificación formal clásicas, que permiten demostrar matemáticamente propiedades de correctitud de un modelo, si bien proveen garantías fuertes, pueden resultar imprácticas o incluso imposibles de aplicar en sistemas completos de escala industrial. Como respuesta a este problema, el área de Runtime Verification estudia cómo generar monitores a partir de especificaciones declarativas, con el objetivo de analizar la traza de una (única) ejecución para verificar su correctitud. Con el tiempo, fueron surgiendo enfoques más expresivos que permiten realizar análisis más complejos, como es el caso de Lola, un lenguaje de especificación junto con algoritmos para el monitoreo de sistemas síncronos. Desde su publicación en 2005, han surgido numerosos trabajos basados en este lenguaje. Uno de los más recientes es hLola, un lenguaje de dominio específico embebido en Haskell para escribir especificaciones junto con un motor para ejecutar los monitores. Esta implementación presenta varias características atractivas, entre las que se destaca la extensibilidad del lenguaje a nuevos tipos de datos, algo no muy habitual en la mayoría de los lenguajes de Runtime Verification. A partir de estos antecedentes y de la experiencia de uso del lenguaje C en sistemas críticos, esta tesina presenta un lenguaje de dominio específico embebido en Haskell, llamado MCLola, para la síntesis de monitores C a partir de especificaciones de alto nivel basadas en el lenguaje Lola.