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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Ramirez, Aldana
Otros Autores: Sánchez, César
Formato: bachelorThesis Tésis de Grado
Lenguaje:Español
Publicado: Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario 2022
Materias:
runtime verification
stream runtime verification
generación de código
lenguaje de dominio específico
programación funcional
Acceso en línea:http://hdl.handle.net/2133/25055
http://hdl.handle.net/2133/25055
Aporte de:
Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR) de Universidad Nacional de Rosario
id I15-R121-2133-25055
record_format dspace
institution Universidad Nacional de Rosario
institution_str I-15
repository_str R-121
collection Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR)
language Español
topic runtime verification
stream runtime verification
generación de código
lenguaje de dominio específico
programación funcional
spellingShingle runtime verification
stream runtime verification
generación de código
lenguaje de dominio específico
programación funcional
Ramirez, Aldana
Generación de monitores C embebidos para especificaciones Lola
topic_facet runtime verification
stream runtime verification
generación de código
lenguaje de dominio específico
programación funcional
description 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.
author2 Sánchez, César
author_facet Sánchez, César
Ramirez, Aldana
format bachelorThesis
Tésis de Grado
author Ramirez, Aldana
author_sort Ramirez, Aldana
title Generación de monitores C embebidos para especificaciones Lola
title_short Generación de monitores C embebidos para especificaciones Lola
title_full Generación de monitores C embebidos para especificaciones Lola
title_fullStr Generación de monitores C embebidos para especificaciones Lola
title_full_unstemmed Generación de monitores C embebidos para especificaciones Lola
title_sort generación de monitores c embebidos para especificaciones lola
publisher Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario
publishDate 2022
url http://hdl.handle.net/2133/25055
http://hdl.handle.net/2133/25055
work_keys_str_mv AT ramirezaldana generaciondemonitorescembebidosparaespecificacioneslola
bdutipo_str Repositorios
_version_ 1764820412614574080

Ejemplares similares