Formale Verifikation von Contiki-Anwendungen

Diese Arbeit stellt einen Ansatz zur formalen Verifikation von eingebetteten Systemen vor. Die betrachteten Software-Anwendungen basieren dabei auf dem eingebetteten Betriebssystem Contiki. Wir stellen unseren Ansatz vor, der Software Model Checking verwendet, zeigen, wie Betriebssystemfunktionen und Treiber abstrahiert werden müssen, um eine Verifikation durchführen zu können, und diskutieren Verifikationsergebnisse für eine Beispielanwendung.