Model checking interrupt-dependent software

Embedded control programs are hard to analyse because their behaviour depends on how they interact with hard-ware devices. In particular, embedded code typically uses interrupts to respond to external events in a timely man-ner. Such asynchronous control constructs make static anal-ysis difficult due to the potentially large number of alter-native control-flow paths they allow. We show how model checking can be used to effectively analyse the behaviour of interrupt-dependent programs. This is done by develop-ing an abstraction of the code that captures its essential timing and functional properties, including those related to external interrupts. The model is made efficient by grouping program instructions into basic blocks whose behaviour is atomic with respect to interrupts.