guest ::
Synthesis of state space generators for model checking microcontroller code = Synthese von Zustandsraum-Generatoren für das Model-Checking von Mikrocontroller-Code
2014 & 2015
Aachen, Techn. Hochsch., Diss., 2014
Druckausgabe: 2014. - Onlineausgabe: 2015. Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University.
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2014-10-15
Online
URN: urn:nbn:de:hbz:82-opus-52966
URL: https://publications.rwth-aachen.de/record/464374/files/5296.pdf
URL: https://publications.rwth-aachen.de/record/464374/files/5296.pdf?subformat=pdfa
Einrichtungen
- Lehrstuhl für Informatik 11 (Software für eingebettete Systeme) (122810)
- Fachgruppe Informatik (120000)
Inhaltliche Beschreibung (Schlagwörter)
Mikrocontroller (Genormte SW) ; Eingebettetes System (Genormte SW) ; Informatik (Genormte SW) ; Informatik (frei) ; Formale Verifikation (frei) ; Model-Checking (frei) ; Retargeting (frei) ; Hardware-Beschreibung (frei) ; Eingebettete Software (frei) ; formal verification (frei) ; hardware description (frei) ; embedded software (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Die Implementierung von Software für eingebettete Systeme erfordert strenge Maßnahmen zur Qualitätssicherung. Der Grund hierfür ist, daß Fehler in dieser Art von Software sehr teuer werden oder gar katastrophale Auswirkungen haben können. Hieraus motiviert sich der Einsatz formaler Methoden zur Verifikation von Software, wie etwa Model-Checking, Theorem Proving, oder statischer Analysen. Viele eingebettete Systeme basieren entweder auf applikationsspezifischen Schaltungen, rekonfigurierbarer Logik, oder Mikrocontrollern. Typischerweise bieten die Hersteller von Mikrocontrollern eine Vielzahl verschiedener Geräte mit der gleichen Kernarchitektur an, die sich im Hinblick auf die verfügbare Ausstattung unterscheiden. Darüber hinaus gibt es Software-Werkzeuge, mit denen Entwickler bestehende Mikrocontroller an ihre eigenen Anforderungen anpassen oder sogar bei Bedarf neue Architekturen entwickeln können. Aus der Vielfalt an verfügbaren Geräten ergeben sich allerdings auch Nachteile. Die Möglichkeit zur automatisierten formalen Verifikation wird eingeschränkt, weil die dafür benötigten Werkzeuge zunächst einmal an jede neue Plattform angepaßt werden müssen. Je nach Werkzeug kann dies auch bedeuten, daß eine komplette Neuimplementierung nötig wird. Das Thema dieser Dissertation ist die Reduktion des Aufwandes, der nötig ist, um ein Verifikationswerkzeug an neue Mikrocontroller anzupassen. Zu diesem Zweck haben wir eine Sprache zur Beschreibung von Mikrocontrollern entworfen, SGDL, und einen Compiler implementiert, der Beschreibungen in dieser Sprache übersetzen kann in funktionsfähige Simulatoren und statische Analyse-Werkzeuge. Unsere Arbeit basiert auf [mc]square, einer Plattform für das Model-Checking und die statische Analyse von Assembler-Code. Um das Problem der Zustandsexplosion zu begrenzen, ist es erforderlich, daß die generierten Simulatoren auch Abstraktionstechniken unterstützen. Anhand einer Reihe von Abstraktionstechniken zeigen wir, wie diese in den vorgestellten Ansatz integriert werden können, und inwieweit es möglich ist, sie ganz oder teilweise automatisch zu erzeugen. In unseren Fallstudien demonstrieren wir die Implementierung von Simulatoren mit unserer neuen Sprache. Darüber hinaus untersuchen wir die Wirksamkeit der bereits genannten Abstraktionstechniken in den generierten Simulatoren, und vergleichen die Ergebnisse mit denen von handgeschriebenen Simulatoren.Creating software for embedded systems requires rigid quality measures. The reason for this is that errors in the software may have very expensive or even disastrous consequences. This gives rise to the use of formal methods for software verification, such as model checking, theorem proving, and static analysis. Many embedded systems rely on either application-specific circuits, reconfigurable logics, or microcontrollers. Manufacturers of microcontrollers typically offer a wide variety of devices based on the same core architecture, which are equipped differently and thus offer different functionality. Furthermore, some tool chains exist that allow developers not only to choose from such off-the-shelf devices, but to customize them for specific kinds of tasks. In some cases, this may go to the extent of actually designing new architectures. It is precisely this wide variety of available devices that complicates the use of automated verification. Tools need to be adapted to a new platform, or even recreated in case they should be implemented in a too hardware-dependent way. The topic this thesis deals with is the reduction of the necessary effort for adapting a verification tool to new microcontrollers. To this end, we designed a language for describing microcontrollers, SGDL, and a compiler for translating such descriptions into operative simulators and static analyzers. We based our work on [mc]square, which is a platform for model checking and static analysis of assembly code software. In order to counter the state explosion problem, it is also necessary to include abstractions in generated simulators. We illustrate, on a number of abstraction techniques, how they can be integrated into the approach and whether they can be generated either partly or entirely. A number of case studies concerning the implementation of simulators with our new language is presented. Additionally, we examine the effectiveness of the aforementioned abstractions that are integrated into the generated simulators, and compare the results to those obtained when using manually implemented simulators.
Fulltext: 
PDF 
PDF (PDFA)
(additional files)
Dokumenttyp
Dissertation / PhD Thesis/Book
Format
online, print
Sprache
English
Externe Identnummern
HBZ: HT018578647
Interne Identnummern
RWTH-CONV-207070
Datensatz-ID: 464374
Beteiligte Länder
Germany
|
The record appears in these collections: |