Defensa Tesis Licenciatura Bruno Gomez
agosto 18 @ 3:00 pm - 4:00 pm
Título: Integración de síntesis reactiva simbólica en MTSA mediante controladores generados por Spectra
Director: Hernán Gagliardi
Jurados: Florencia Zanollo, Sebastian Uchitel
Director: Hernán Gagliardi
Jurados: Florencia Zanollo, Sebastian Uchitel
Resumen
Esta tesis estudia la integración entre MTSA y Spectra para incorporar capacidades de síntesis reactiva simbólica dentro de un flujo basado en modelos LTS. En particular, se propone una traducción desde modelos expresados en MTSA hacia especificaciones Spectra, la invocación del motor de síntesis de Spectra, y la posterior reconstrucción de uncontrolador en formato LTS a partir de la representación simbólica generada.
El objetivo general es explorar cómo aprovechar controladores representados mediante BDDs y técnicas de exploración just-in-time para producir artefactos compatibles con MTSA, preservando una semántica útil para el análisis, la composición y la inspección de controladores.
Esta tesis estudia la integración entre MTSA y Spectra para incorporar capacidades de síntesis reactiva simbólica dentro de un flujo basado en modelos LTS. En particular, se propone una traducción desde modelos expresados en MTSA hacia especificaciones Spectra, la invocación del motor de síntesis de Spectra, y la posterior reconstrucción de uncontrolador en formato LTS a partir de la representación simbólica generada.
El objetivo general es explorar cómo aprovechar controladores representados mediante BDDs y técnicas de exploración just-in-time para producir artefactos compatibles con MTSA, preservando una semántica útil para el análisis, la composición y la inspección de controladores.
