Vörtler, ThiloThiloVörtlerHöckner, BennyBennyHöcknerHofstedt, PetraPetraHofstedtKlotz, ThomasThomasKlotz2022-03-122022-03-122015https://publica.fraunhofer.de/handle/publica/388111Diese 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.de621004conference paper