RT Generic
T1 Modelado y análisis de un sistema de semáforos inteligentes con UPPAAL
T2 Modelling and analysis for an intelligent traffic lights system with UPPAAL
A1 Villarejo Pérez, Pablo
K1 Informática - Trabajos Fin de Grado
K1 Grado en Ingeniería del Software - Trabajos Fin de Grado
AB En este Trabajo de Fin de Grado se aborda el análisis y verificación formal deun sistema de semáforos inteligentes aplicado a un cruce complejo en el campusuniversitario de Teatinos (Universidad de Málaga), donde confluyen vehículos,metro en superficie y ambulancias debido a la cercanía del hospital. El objetivoprincipal 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 empleaUPPAAL, una herramienta de model checking que permite modelar, simulary verificar sistemas de tiempo real mediante autómatas temporizados y autómatastemporizados estocásticos.El trabajo se desarrolla de forma iterativa, comenzando con un modelo básicoque incluye coches, metro y semáforos, y ampliándose posteriormente conun segundo cruce regulado y, finalmente, incluyendo también ambulancias. A lolargo de estas iteraciones se definen requisitos, se modelan las restricciones y severifican propiedades de seguridad, viveza y rendimiento, tanto con verificaciónexhaustiva como con verificación estocástica. Los resultados muestran que losmétodos formales permiten no solo detectar errores tempranos en el diseño, sinotambién garantizar de manera rigurosa la corrección y robustez de un sistemacrítico como el control de tráfico urbano.
YR 2025
FD 2025-09
LK https://hdl.handle.net/10630/46117
UL https://hdl.handle.net/10630/46117
LA spa
DS RIUMA. Repositorio Institucional de la Universidad de Málaga
RD 7 abr 2026