Dominique Gückel
2008-10-22 09:20:42 UTC
Motivation:
Am Lehrstuhl Informatik 11 (Software für eingebettete Systeme) wurde und
wird ein Model-Checker für Mikrocontroller-Code namens [mc]square
entwickelt. [mc]square ist ein CTL-Model-Checker, der als Eingabe ein
Assembler- oder C-Programm erwartet. Der Zustandsraum des Model-Checkers
entsteht (vereinfacht ausgedrückt) durch die Ausführung des Programms
durch einen Simulator für den jeweiligen Mikrocontroller. Derzeit
verfügt [mc]square über Simulatoren für
* Atmel ATmega16
* Atmel ATmega128
* Intel 8051
* Infineon XC167
Einige dieser Simulatoren sind das Ergebnis von Diplomarbeiten. Im
Rahmen eines EU-Forschungsprojektes mit Beteiligung eines
Industrieunternehmens soll nun [mc]square zur Verifikation eines auf
einem Renesas R8C/Tiny basierenden Systems eingesetzt werden. Der dafür
nötige Simulator ist im Rahmen dieser Diplomarbeit zu realisieren.
Aufgabenstellung:
Implementierung eines Simulators für einen Renesas-Mikrocontroller. Bei
dem Mikrocontroller handelt es sich um einen Renesas R8C/Tiny,
voraussichtlich den R8C/Tiny \23. Der fertige Simulator sollte zumindest
den Befehlssatz des Mikrocontrollers verarbeiten können. Weitere
On-Chip-Peripherie ist wünschenswert, aber nicht unbedingtes Ziel.
Ziel der Arbeit:
Implementierung des Simulators, Einsatz des Model-Checkers im
Industrieprojekt.
Studienrichtung:
Informatik (Diplomstudiengang)
Vorkenntnisse:
Java
Grundkenntnisse der Mikrocontroller-Programmierung
Bei Interesse wende dich einfach mit aussagekräftigen Dokumenten
(aktueller Notenspiegel, kurzer Lebenslauf) an
Dominique Marcel Gückel
gueckel [at] informatik [dot] rwth-aachen [dot] de
Am Lehrstuhl Informatik 11 (Software für eingebettete Systeme) wurde und
wird ein Model-Checker für Mikrocontroller-Code namens [mc]square
entwickelt. [mc]square ist ein CTL-Model-Checker, der als Eingabe ein
Assembler- oder C-Programm erwartet. Der Zustandsraum des Model-Checkers
entsteht (vereinfacht ausgedrückt) durch die Ausführung des Programms
durch einen Simulator für den jeweiligen Mikrocontroller. Derzeit
verfügt [mc]square über Simulatoren für
* Atmel ATmega16
* Atmel ATmega128
* Intel 8051
* Infineon XC167
Einige dieser Simulatoren sind das Ergebnis von Diplomarbeiten. Im
Rahmen eines EU-Forschungsprojektes mit Beteiligung eines
Industrieunternehmens soll nun [mc]square zur Verifikation eines auf
einem Renesas R8C/Tiny basierenden Systems eingesetzt werden. Der dafür
nötige Simulator ist im Rahmen dieser Diplomarbeit zu realisieren.
Aufgabenstellung:
Implementierung eines Simulators für einen Renesas-Mikrocontroller. Bei
dem Mikrocontroller handelt es sich um einen Renesas R8C/Tiny,
voraussichtlich den R8C/Tiny \23. Der fertige Simulator sollte zumindest
den Befehlssatz des Mikrocontrollers verarbeiten können. Weitere
On-Chip-Peripherie ist wünschenswert, aber nicht unbedingtes Ziel.
Ziel der Arbeit:
Implementierung des Simulators, Einsatz des Model-Checkers im
Industrieprojekt.
Studienrichtung:
Informatik (Diplomstudiengang)
Vorkenntnisse:
Java
Grundkenntnisse der Mikrocontroller-Programmierung
Bei Interesse wende dich einfach mit aussagekräftigen Dokumenten
(aktueller Notenspiegel, kurzer Lebenslauf) an
Dominique Marcel Gückel
gueckel [at] informatik [dot] rwth-aachen [dot] de
--
Dipl.-Inform. Dominique Marcel Gückel
RWTH Aachen, Lehrstuhl Informatik 11 - Software für eingebettete Systeme
Ahornstraße 55, 52074 Aachen
fon: +049 0241 80 21168
fax: +049 0241 80 22150
mail: gueckel [at] informatik [dot] rwth-aachen [dot] de
web: http://www-i11.informatik.rwth-aachen.de
Dipl.-Inform. Dominique Marcel Gückel
RWTH Aachen, Lehrstuhl Informatik 11 - Software für eingebettete Systeme
Ahornstraße 55, 52074 Aachen
fon: +049 0241 80 21168
fax: +049 0241 80 22150
mail: gueckel [at] informatik [dot] rwth-aachen [dot] de
web: http://www-i11.informatik.rwth-aachen.de