Environmental Simulation of Real-Time Systems with Nested Interrupts

Interrupts are important aspects of real-time embedded systems to handle events in time. When there exist nested interrupts in a real-time system, and an urgent interrupt is allowed to preempt the current interrupt handling, the design and analysis of the system become difficult due to the lack of appropriate behavioral models. This paper proposes a compositional model for nested interrupts and an analysis named environmental simulation. We present a new kind of timed transition system, named controller automata, to treat interrupts. Together with an interrupt environment modeled as a timed automaton, and a scheduler as a timed automaton with semaphores, the system behaviors with nested interrupts are realized by a sequence of transitions with time. Although various verification problems for this model are undecidable in general, it is shown that the reachability of error states is practically solvable with our implementation of the environmental simulation by Maude.