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 in-terrupts in a real-time system, and an urgent interrupt is al-lowed 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 automa-ton with semaphores, the system behaviors with nested in-terrupts 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 to error states is practically solvable with our implementation of the environmental simulation by Maude. 1