Model checking of software for microcontrollers

Schlich, Bastian; Kowalewski, Stefan

doi:0935-3232

Model checking of software for microcontrollers = Model-Checking von Software für Mikrocontroller

Schlich, Bastian (Author)

2008

Verantwortlichkeitsangabevorgelegt von Bastian Schlich

ImpressumAachen : RWTH Aachen, Department of Computer Science 2008

UmfangIV, 159 S. : graph. Darst.

ReiheAachener Informatik-Berichte ; 2008,14

Zugl.: Aachen, Techn. Hochsch., Diss., 2008

Zsfassung in engl. und dt. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Kowalewski, Stefan (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2008-06-04

Online
URN: urn:nbn:de:hbz:82-opus-24308
URL: https://publications.rwth-aachen.de/record/63747/files/Schlich_Bastian.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Model checking (Genormte SW) ; Quellcode (Genormte SW) ; Mikrocontroller (Genormte SW) ; Statische Analyse (Genormte SW) ; Informatik (frei) ; Source Code (frei) ; Microcontroller (frei) ; Static Analysis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Software für Mikrocontroller wird immer komplexer. Es ist wichtig, die Software für Mikrocontroller ausführlich zu testen, da Fehler schwerwiegende Folgen haben und hohe Kosten verursachen können. Model-Checking ist eine formale Methode, um zu verifizieren, ob ein System bestimmte Eigenschaften erfüllt. Diese Arbeit beschreibt ein neues Vorgehen, um Model-Checking auf Software für Mikrocontroller anzuwenden. In diesem Vorgehen wird der Assembler Code anstatt einer Zwischendarstellung wie z.B. des C Codes überprüft. Die Entwicklung des Model Checkers [mc]square, welcher diesen neuen Ansatz implementiert, wird detailiert beschrieben. [mc]square hat eine modulare Architektur, um das Problem der Hardwareabhängigkeit zu umgehen. Die verschiedenen Schritte des Model-Checking Prozesses sind in verschiedene Pakete aufgeteilt. Die Erstellung des Zustandsraums wird durch einen speziellen Simulator durchgeführt, welcher die einzige hardwareabhängige Komponente von [mc]square ist. Diese Arbeit beschreibt die Modellierung des ATMEL ATmega16 Mikrocontrollers und detailiert die verschiedenen implementierten Abstraktionstechniken, welche benutzt werden um das Problem der Zustandsexplosion zu bekämpfen. Diese Abstraktionstechniken beinhalten lazy interrupt evaluation, lazy stack evaluation, delayed nondeterminism, dead variable reduction und path reduction. Delayed nondeterminism führt symbolische Zustände ein, die eine Menge von konkreten Zuständen repräsentieren. Es werden trotzdem explizite Model-Checking Techniken verwendet. Also haben wir erfolgreich explizite und symbolische Model-Checking Techniken kombiniert. Weiterhin wird ein formales Modell des Simulators beschrieben, welches wir entwickelt haben, um die Korrektheit der Abstraktionstechniken zu beweisen. Um zu zeigen, dass der beschriebene Ansatz funktioniert, beschreiben wir zwei Fallstudien, in denen wir Programme unterschiedlicher Größen überprüft haben. Die verwendeten Programme wurden alle von Studenten in Übungen, Praktika oder während Diplomarbeiten erstellt, ohne die Absicht diese später durch Model-Checking zu überprüfen.

Software of microcontrollers is getting more and more complex. It is mandatory to extensively analyze their software as errors can lead to severe failures or cause high costs. Model checking is a formal method used to verify whether a system satisfies certain properties. This thesis describes a new approach for model checking software for microcontrollers. In this approach, assembly code is used for model checking instead of an intermediate representation such as C code. The development of [mc]square, which is a microcontroller assembly code model checker implementing this approach, is detailed. [mc]square has a modular architecture to cope with the hardware dependency of this approach. The single steps of the model checking process are divided into separate packages. The creation of the states is conducted by a specific simulator, which is the only hardware-dependent package. Within the simulator, the different microcontrollers are modeled accurately. This work describes the modeling of the ATMEL ATmega16 microcontroller and details implemented abstraction techniques, which are used to tackle the state-explosion problem. These abstraction techniques include lazy interrupt evaluation, lazy stack evaluation, delayed nondeterminism, dead variable reduction, and path reduction. Delayed nondeterminism introduces symbolic states, which represent a set of states, into [mc]square while still explicit model checking techniques are used. Thus, we successfully combined explicit and symbolic model checking techniques. A formal model of the simulator, which we developed to prove the correctness of abstraction techniques, is described. In this work, the formal model is used to show the correctness of delayed nondeterminism. To show the applicability of the approach, two case studies are described. In these case studies, we used programs of different sizes. All these programs were created by students in lab courses, during diploma theses, or in exercises without the intention to use them for model checking.

Fulltext:
PDF