Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Formal verification of software for the Contiki operating system considering interrupts

 
: Vörtler, Thilo; Höckner, Benny; Hofstedt, Petra; Klotz, Thomas

:

Institute of Electrical and Electronics Engineers -IEEE-:
DDECS 2015, 18th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems : April 22-24, 2015, Belgrade, Serbia
Piscataway, NJ: IEEE, 2015
ISBN: 978-1-4799-6779-7 (ISBN)
S.295-298
Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS) <18, 2015, Belgrade>
Englisch
Konferenzbeitrag
Fraunhofer IIS, Institutsteil Entwurfsautomatisierung (EAS) ()

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.

: http://publica.fraunhofer.de/dokumente/N-341223.html