El algoritmo de Dekker para la exclusión mutua de dos procesos es la conocida primera solución correcta desarrollada basada únicamente en mecanismos de software. El algoritmo sirvió como punto de partida para que los investigadores crearan soluciones seguras posteriores tanto para dos como para N > 2 procesos. En años recientes, Dekker propuso una generalización de su algoritmo de exclusión mutua para N > 2 procesos (aquí referido como Dekker-N). Hasta donde sabemos, la corrección de Dekker-N solo fue demostrada por el autor utilizando argumentos informales. La contribución original de este artículo consiste en el modelado formal y la verificación de Dekker-N utilizando un enfoque basado en autómatas temporizados (TA) y el verificador de modelos Uppaal. El modelo de Dekker-N es verificado bajo registros atómicos y también en casos donde se utilizan registros no atómicos. Este artículo primero demuestra que Dekker-N es correcto y justo con registros atómicos y asegura efectivamente una espera acotada para procesos en competencia a través de un adelantamiento lineal. Desafortunadamente, el algoritmo se vuelve incorrecto cuando se utilizan registros no atómicos. Sin embargo, el enfoque formal adoptado nos permitió demostrar que al hacer que solo una variable común sea segura, Dekker-N resulta ser completamente correcto y justo también con registros no atómicos. El artículo presenta el enfoque formal basado en TA y continúa presentando modelos de Dekker-N y verificando todas sus propiedades de exclusión mutua.