Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Formale Verifikation von eingebetteter Software für das Betriebssystem Contiki unter Berücksichtigung von Interrupts

 
: Vörtler, Thilo

Heinkel, U. ; TU Chemnitz, Fakultät für Elektrotechnik und Informationstechnik:
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV 2015. Tagungsband : 03.03. - 04.03.2015, Mercure Hotel Kongress Chemnitz, Workshop
Chemnitz: Technische Universität Chemnitz, 2015
ISBN: 978-3-00-048889-4
S.20-29
Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV) <17, 2014, Böblingen>
Deutsch
Konferenzbeitrag
Fraunhofer IIS, Institutsteil Entwurfsautomatisierung (EAS) ()

Abstract
Diese Arbeit stellt einen Ansatz für die formale Verifikation von Anwendungen für das Betriebssystem Contiki basierend auf Software-Model-Checking vor. Insbesondere die Verwendung von Interrupts muss bei der Modellierung des Systemverhaltens beachtet werden. Nach einer Beschreibung des Contiki-Systems, werden verschiedene Ansätze zur Modellierung von Interrupts diskutiert und ein Vorgehen abgleitet, wie Anwendungen für Contiki mit Hilfe des Model-Checking-Tools CBMC überprüft werden können.

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