Title :
Formal Verification of Software for the Contiki Operating System Considering Interrupts
Author :
Vortler, Thilo ; Hockner, Benny ; Hofstedt, Petra ; Klotz, Thomas
Author_Institution :
Design Autom. Div., Fraunhofer Insitute for Integrated Circuits, Germany
Abstract :
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.
Keywords :
C language; embedded systems; interrupts; operating systems (computers); program verification; source code (software); CBMC; Contiki operating system; embedded system operating system; formal verification framework; hardware environment; hardware independent C source code; interrupt handling; periodically-occurring interrupts; software model checking tool; Embedded systems; Kernel; Model checking; Radiation detectors; Random access memory;
Conference_Titel :
Design and Diagnostics of Electronic Circuits & Systems (DDECS), 2015 IEEE 18th International Symposium on
Conference_Location :
Belgrade
Print_ISBN :
978-1-4799-6779-7
DOI :
10.1109/DDECS.2015.59
