Formal Verification of Software for the Contiki Operating System Considering Interrupts

In this work we present a verification framework for applications for the embedded system operating system Contiki, based on the software model checking tool CBMC. A challenge when verifying such systems is the modeling of the hardware environment, especially the handling of interrupts. After an introduction to the Contiki system, we discuss approaches to model interrupts at the level of hardware independent C source code and present a new modeling approach for periodically occurring interrupts. Finally, verification results for these approaches based on different Contiki applications are presented.