Análisis de la sincronización del protocolo PTP utilizando Uppaal.

Abstract

La sincronización precisa del tiempo es esencial en los sistemas distribuidos, especialmente en redes 5G, automatización industrial y aplicaciones en tiempo real [1, 2]. El protocolo Precision Time Protocol (PTP), definido en el estándar IEEE 1588-2019 [3], permite una alineación exacta de los relojes a través de redes conmutadas por paquetes. Este trabajo presenta un modelo formal del proceso de sincronización de PTP, desarrollado mediante autómatas temporizados en el entorno UPPAAL [4]. El modelo se construye bajo condiciones ideales como la ausencia de retardo en la transmisión de mensajes con el fin de aislar la lógica del protocolo y verificar su corrección. Se evalúan propiedades de seguridad, vivacidad y convergencia utilizando técnicas de verificación estadística [5]. Además, se compara el modelo inspirado en PTP con variantes simplificadas de algoritmos de sincronización ampliamente conocidos (PID, filtro de Kalman y PLL) [6, 7, 8], evaluando su eficiencia y robustez. Los resultados ponen de relieve el potencial de los métodos formales para analizar protocolos de comunicación, aportando ideas para la optimización de PTP en sistemas sensibles al tiempo, así como los retos derivados de las limitaciones de ciertas herramientas a la hora de modelar comportamientos dependientes del tiempo.