Al verificar programas para sistemas integrados, es esencial reducir el tiempo de verificación porque puede ocurrir una explosión de estados durante la comprobación del modelo. Una solución es reducir el número de ejecuciones de manejadores de interrupciones. En particular, cuando se incorporan interrupciones periódicas como las interrupciones de temporizador, es necesario conocer el tiempo físico. En este documento, definimos un autómata de flujo de control (CFA) que puede manejar el tiempo y proponemos un algoritmo basado en la reducción de ejecuciones de manejadores de interrupciones (IHER). El método propuesto reduce el número de ejecuciones de interrupciones, incluidas las interrupciones de temporizador. Un estudio de caso verificó la efectividad de este algoritmo.