Sciweavers

APSEC
2005
IEEE

Model Checking Interrupt-Dependent Software

13 years 9 months ago
Model Checking Interrupt-Dependent Software
Embedded control programs are hard to analyse because their behaviour depends on how they interact with hardware devices. In particular, embedded code typically uses interrupts to respond to external events in a timely manner. Such asynchronous control constructs make static analysis difficult due to the potentially large number of alternative 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 developbstraction 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.
Colin J. Fidge, Phil Cook
Added 24 Jun 2010
Updated 24 Jun 2010
Type Conference
Year 2005
Where APSEC
Authors Colin J. Fidge, Phil Cook
Comments (0)