Automata-based modeling of interrupts in the Linux PREEMPT RT kernel