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

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.