Model checking of software for microcontrollers [Elektronische Ressource] / vorgelegt von Bastian Schlich

Dipl.-Inform. Bastian Schlich

Sujets

• Informatik

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2008
• Nombre de lectures: 16
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Aachen
Department of Computer Science
Technical Report
Model Checking of Software for
Microcontrollers
Bastian Schlich
ISSN 0935{3232 Aachener Informatik Berichte AIB-2008-14
RWTH Aachen Department of Computer Science June 2008The publications of the Department of Computer Science of RWTH Aachen
University are in general accessible through the World Wide Web.
http://aib.informatik.rwth-aachen.de/Model Checking of Software for
Microcontrollers
Von der Fakultät für Mathematik, Informatik und
Naturwissenschaften der RWTH Aachen University
zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Informatiker
Bastian Schlich
aus
Essen/Ruhr
Berichter: Professor Dr.-Ing. Stefan Kowalewski Dr. Jan Peleska
Tag der mündlichen Prüfung: 04.06.2008
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online verfügbar.Abstract
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 microcon-
trollers. 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 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.Acknowledgments
First and foremost, I would like to thank Professor Dr.-Ing. Stefan Kowalewski for
giving me the opportunity to join his group to write my Dissertation thesis. He
provided me great degrees of freedom to find my own topic and assisted me making
important decisions. He was always willing to listen to my problems and gave me
many useful advices.
I thank Professor Dr. Jan Peleska for his willingness to be part of my Promotions-
komission. Moreover, I thank him for the invitations to Bremen during which we
had many fruitful discussions.
I sincerely thank all members of Informatik 11 for the friendly working atmosphere,
which contributed a lot to this thesis. Particularly, I have to thank my friends
and colleagues Daniel Klünder, Falk Salewski, and Dirk Wilking for many fruitful
discussions and for answering a pledora of questions both related and unrelated to my
Dissertation thesis. Furthermore, I thank Dr. Carsten Weise for many useful hints
and advices during the final phase of my thesis. I thank my students Lucas Brutschy,
Eduard Feicho, Dominique Gückel, Volker Kamin, Jann Löll, Michael Rohrbach,
Florian Scheuer, and John Schommer for helping me to implement [mc]square.
I gratefully thank Dr. Thomas Noll for his support during the last year. He helped
me to get a more formal insight of delayed nondeterminism and gave me many useful
advices for my thesis. He always took the time to answer my numerous questions.
I thank Dr. Ralf Huuck for inviting me to Australia. We had many interesting
discussions and his pragmatism helped me to solve some of the problems that
arise when writing a Dissertation thesis. Furthermore, I thank all colleagues of the
Managing Complexity program at the National ICT Australia in Sydney. Especially,
I thank Timothy Bourke, Jörg Brauer, Dr. Ansgar Fehnker, Dr. Gerwin Klein, Rafal
Kolanski, and Harvey Tuch for many discussions and their valuable comments about
my thesis.
I appreciate Dr. Michael Weber’s contribution in the initial phase of my Disserta-
tion thesis. He helped me discovering the peculiarities of assembly code.
Last but not least, I would like to thank my family. They always supported me
and helped my to find my way. Without them, this thesis would not have been
possible.
Bastian Schlich
Aachen, June 2008Contents
1 Introduction 1
1.1 Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.4 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.5 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2 Preliminaries 7
2.1 Computation Tree Logic . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2.1 Explicit vs. Symbolic Model Checking . . . . . . . . . . . . . 10
2.2.2 Global vs. Local Model Checking . . . . . . . . . . . . . . . . 11
2.2.3 Counterexamples & Witnesses . . . . . . . . . . . . . . . . . 11
2.3 Static Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3 Model Checking Software for Microcontrollers 13
3.1 Model Checking C Code . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.2 Model Checking Assembly Code . . . . . . . . . . . . . . . . . . . . 16
3.3 Requirements for an Assembly Code Model Checker . . . . . . . . . 18
4 [mc]square 21
4.1 Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
4.2 Architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
4.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
5 State Space Building in [mc]square 29
5.1 Simulator Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5.2 Sim State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5.3 Microcontroller . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5.3.1 Core . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5.3.2 Memories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5.3.3 Stack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5.3.4 Interrupts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5.3.5 I/O Ports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
iContents
5.3.6 Timers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
5.4 Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
5.5 Instruction Simulator . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.6 Determinizer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
5.6.1 Determinizer Overview . . . . . . . . . . . . . . . . . . . . . . 53
5.6.2 Immediate Instantiation . . . . . . . . . . . . . . . . . . . . . 56
5.6.3 Delayed Nondeterminism . . . . . . . . . . . . . . . . . . . . 58
5.7 Formal Model of the Simulator . . . . . . . . . . . . . . . . . . . . . 62
5.7.1 Handlers and Guarded Assignments . . . . . . . . . . . . . . 63
5.7.2 Modeling the ATMEL ATmega16 . . . . . . . . . . . . . . . . 65
5.7.3 Coping with Nondeterminism . . . . . . . . . . . . . . . . . . 67
5.7.4 Establishing Correctness . . . . . . . . . . . . . . . . . . . . . 70
5.8 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
5.8.1 Model Checking Machine Code . . . . . . . . . . . . . . . . . 71
5.8.2 Delayed Nondeterminism . . . . . . . . . . . . . . . . . . . . 73
6 Static Analysis in [mc]square 75
6.1 Challenges in Static Analysis of Assembly Code . . . . . . . . . . . . 75
6.2 Static Analyzer Overview . . . . . . . . . . . . . . . . . . . . . . . . 77
6.3 Analyses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.3.1 Control Flow Analysis . . . . . . . . . . . . . . . . . . . . . . 79
6.3.2 Live Variables . . . . . . . . . . . . . . . . . . . . . 81
6.3.3 Reaching Definitions Analysis . . . . . . . . . . . . . . . . . . 84
6.3.4 Stack Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 86
6.3.5 Global Interrupt Flag Analysis . . . . . . . . . . . . . . . . . 88
6.4 Abstraction Techniques . . . . . . . . . . . . . . . . . . . . . . . . . 90
6.4.1 Dead Variable Reduction . . . . . . . . .