An Overtime-Detection Model-Checking Technique for Interrupt Processing Systems

Abstract

This paper presents an overtime-detection model-checking technique for interrupt processing systems. It is very important to verify real-time properties of such systems because many of them are safety-critical. This paper gives a method to check that critical interrupts can be handled within their timeout periods. Interrupt processing systems are modeled as extended timed automata. Our technique checks whether the system under check can handle critical interrupts in time using symbolic model-checking techniques. Taking an aerospace control system as an example, we show that our technique can find time-scheduling problems in interrupt processing systems. © Springer-Verlag Berlin Heidelberg 2013.