Defensa Tesis Licenciatura Fernando Otero

• Título: Emulando el orden de exploración BFS en el model checking distribuido de autómatas temporizados
• Director: Fernando Schapachnik
• Jurados: Esteban Pavese y Sergio Yovine
• Resumen:

Los sistemas de tiempo real están presentes en una gran cantidad de aplicaciones que van desde sistemas financieros hasta controladores de aviones o protocolos de comunicaciones. Tiene un gran número de ventajas sobre las soluciones tradicionales que están basadas en simulación, pruebas y razonamiento deductivo. En particular, el Model Checking es automático y suele ser más rápido. La complejidad de los mismos es cada día mayor debido al aumento de la criticidad de las funciones que realizan, lo que también agrava los problemas generados por las fallas. Es por esto que vale la pena realizar análisis rigurosos de sus especificaciones para poder asegurar un buen diseño e intentar garantizar que ciertas propiedades se cumplen. A este tipo de análisis se lo suele llamar Verificación Automática o Model Checking. Un formalismo muy difundido para realizar Model Checking es el de los autómatas temporizados, una extensión de la teoría clásica de autómatas que permite trabajar con tiempo denso. Las técnicas para analizarlos son conocidas desde hace ya bastante tiempo, pero tienen la desventaja de baja escalabilidad lo cual dificulta su uso en los sistemas actuales.

Una de los grandes dificultades de los Model Checkers Temporizados es que un problema de tamaño mediano puede acabar rápidamente con los recursos disponibles en una computadora aún siendo ésta muy poderosa El problema de chequeo de propiedades con autómatas temporizados es PSPACE-complete (ver [ACD93] 5.5 para la prueba formal). Por esta razón en los últimos años se han realizado trabajos para intentar versiones distribuidas de los Model Checkers existentes. Otra de las dificultades principales, que es inherente a las estructuras de datos utilizadas, es la fragmentación [Beh03]. La fragmentación es un fenómeno generador de graves inconvenientes de performance, y consiste básicamente en que al distribuir el algoritmo de verificación se descubren muchos más estados que en la versión no paralela.

En el presente trabajo, que intenta proponer formas de solucionar el problema de la fragmentación, se presentan primero las definiciones preliminares necesarias para entender el problema, y luego se analiza el estado actual del mismo. En la sección de experimentación se explican las técnicas investigadas para luego revisar los resultados obtenidos, terminando con conclusiones e ideas para futuras mejoras.