RT Generic
T1 Análisis de la sincronización del protocolo PTP utilizando Uppaal.
T2 Analysis of PTP protocol synchronization using Uppaal.
A1 Guerrero Rico, Javier
K1 Informática - Trabajos Fin de Grado
K1 Grado en Ingeniería Informática - Trabajos Fin de Grado
AB La sincronización precisa del tiempo es esencial en los sistemas distribuidos,especialmente en redes 5G, automatización industrial y aplicaciones en tiemporeal [1, 2]. El protocolo Precision Time Protocol (PTP), definido en el estándarIEEE 1588-2019 [3], permite una alineación exacta de los relojes a través de redesconmutadas por paquetes. Este trabajo presenta un modelo formal del procesode sincronización de PTP, desarrollado mediante autómatas temporizados en elentorno UPPAAL [4].El modelo se construye bajo condiciones ideales como la ausencia de retardoen la transmisión de mensajes con el fin de aislar la lógica del protocolo y verificarsu corrección. Se evalúan propiedades de seguridad, vivacidad y convergenciautilizando técnicas de verificación estadística [5]. Además, se compara el modeloinspirado en PTP con variantes simplificadas de algoritmos de sincronización ampliamenteconocidos (PID, filtro de Kalman y PLL) [6, 7, 8], evaluando su eficienciay robustez.Los resultados ponen de relieve el potencial de los métodos formales para analizarprotocolos de comunicación, aportando ideas para la optimización de PTPen sistemas sensibles al tiempo, así como los retos derivados de las limitacionesde ciertas herramientas a la hora de modelar comportamientos dependientes deltiempo.
YR 2025
FD 2025
LK https://hdl.handle.net/10630/45979
UL https://hdl.handle.net/10630/45979
LA spa
DS RIUMA. Repositorio Institucional de la Universidad de Málaga
RD 21 mar 2026