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 envi ronmental simulation by Maude.
Guoqiang Li Shoji Yuen Masakazu Adachi
BASICS, Shanghai Jiao Tong University Shanghai China NCES, Nagoya University Nagoya, Japan Toyota Central R&D Labs. INC.Nagoya, Japan
国际会议
天津
英文
21-28
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）