Modelado y análisis de un sistema de semáforos inteligentes con UPPAAL

Abstract

En este Trabajo de Fin de Grado se aborda el análisis y verificación formal de un sistema de semáforos inteligentes aplicado a un cruce complejo en el campus universitario de Teatinos (Universidad de Málaga), donde confluyen vehículos, metro en superficie y ambulancias debido a la cercanía del hospital. El objetivo principal es garantizar la seguridad en el cruce minimizando el riesgo de colisiones, al mismo tiempo que se asegura un flujo vehicular eficiente. Para ello se emplea UPPAAL, una herramienta de model checking que permite modelar, simular y verificar sistemas de tiempo real mediante autómatas temporizados y autómatas temporizados estocásticos. El trabajo se desarrolla de forma iterativa, comenzando con un modelo básico que incluye coches, metro y semáforos, y ampliándose posteriormente con un segundo cruce regulado y, finalmente, incluyendo también ambulancias. A lo largo de estas iteraciones se definen requisitos, se modelan las restricciones y se verifican propiedades de seguridad, viveza y rendimiento, tanto con verificación exhaustiva como con verificación estocástica. Los resultados muestran que los métodos formales permiten no solo detectar errores tempranos en el diseño, sino también garantizar de manera rigurosa la corrección y robustez de un sistema crítico como el control de tráfico urbano.