El trabajo descrito en este documento desarrolla un método formal para modelar y verificar exhaustivamente algoritmos de exclusión mutua. El proceso se basa en autómatas temporizados y en el verificador de modelos Uppaal.