Los algoritmos de exclusión mutua son el corazón de los sistemas concurrentes/paralelos y distribuidos. Es bien sabido que tales algoritmos son muy difíciles de analizar, y en la literatura existen diferentes conjeturas sobre la libertad de inanición y el número de adelantamientos (también llamado factor de adelantamiento). El factor de adelantamiento afecta el tiempo de espera (con suerte) acotado que un proceso compitiendo por entrar en la sección crítica tiene que sufrir antes de acceder al recurso compartido. Este artículo propone un enfoque de modelado novedoso basado en Autómatas Temporizados y el conjunto de herramientas Uppaal, que resulta efectivo para estudiar todas las propiedades de un algoritmo de exclusión mutua para procesos, mediante verificación exhaustiva del modelo. Aunque el enfoque, como ya han confirmado experimentos similares reportados en la literatura, no es escalable debido a problemas de explosión de estados y solo puede aplicarse en la práctica hasta , es de gran valor para revelar las verdaderas propiedades de los algoritmos analizados. Para dimensiones , se puede utilizar el Verificador de Modelos Estadísticos de Uppaal, que, aunque basado en simulaciones, puede confirmar propiedades mediante estimaciones y probabilidades. Este artículo describe el método de modelado y verificación propuesto y lo aplica a varios algoritmos de exclusión mutua, recuperando así propiedades conocidas pero también mostrando nuevos resultados sobre propiedades a menudo estudiadas mediante razonamiento informal.