Interrupt Timed Automata: verification and expressiveness