Dr. rer. nat. Dominique Marcel Gückel

• Ich war von Januar 2008 bis Ende 2010 Promotions-Stipendiat im DFG-Graduiertenkolleg AlgoSyn. Von Januar 2011 bis Oktober 2011 war ich Wissenschaftlicher Mitarbeiter am Lehrstuhl Informatik 11.
• Im Rahmen meines seit 2008 laufenden Promotionsvorhabens erforsche ich, ob und wie gut sich Model-Checker für eingebettete Software an neue Hardwareplattformen anpassen lassen. Gegenstand der Forschung ist der am Lehrstuhl Informatik 11 entwickelte Model-Checker [mc]square, der Programme für Mikrocontroller überprüfen kann.
• Der von mir gewählte Ansatz basiert auf der Verwendung von Hardware-Beschreibungssprachen: statt [mc]square manuell um Simulatoren für neue Mikrocontroller zu erweitern, nehmen wir stattdessen eine Beschreibung der Eigenschaften des Controllers und synthetisieren daraus den Simulator. Dabei sind Besonderheiten wie die Unterstützung von Abstraktionstechniken zu berücksichtigen, damit die synthetisierten Simulatoren ähnlich leistungsfähig sind wie sorgfältig von Hand erstellten. Die Entwicklung einer geeigneten Sprache und des notwendigen Compilers sind Teil der Forschung.
  

• Deutsch (Muttersprache)
• Englisch (fließend)
• Französisch (fließend)
• Latein (Latinum)
• Spanisch (Grundkenntnisse)

• Leitung Proceedings-Gruppe für die Proceedings des Gemeinsamen Workshops der Graduiertenkollegs der Informatik in Dagstuhl, 2010. Druckversion im Buchhandel (ISBN: 386-130-146-6); Online-Version des Bands ist verfügbar als PDF.

• Dominique Gückel: Erweiterung des Model-Checkers [mc]square um benutzerdefinierte Umgebungen. Diplomarbeit, RWTH Aachen, 2007.

• Bastian Schlich, Dominique Gückel, and Stefan Kowalewski. Modeling the Environment of Microcontrollers to Tackle the State-Explosion Problem in Model Checking. In Proceedings of Symposium Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2008), ISBN 978-963-236-138-3. PDF

• Dominique Gückel. Retargeting a Hardware-Dependent Model Checker by Using Architecture Description Languages. In Doctoral Symposium on Systems Software Verification (DS SSV 2009), 4th International Workshop on Systems Software Verification (SSV 09), ISSN 0935–3232. PDF

• Wolfgang Thomas, Kai Bollue, Dominique Gückel, Gustavo Quiros, Michaela Slaats and Michael Ummels. DFG Research Training Group „Algorithmic Synthesis of Reactive and Discrete-Continuous Systems (AlgoSyn)“. In it - Information Technology, Volume 4 /2009, Oldenbourg.
• Dominique Gückel, Bastian Schlich, Jörg Brauer, and Stefan Kowalewski. Synthesizing Simulators For Model Checking Microcontroller Binary Code. In Proceedings of 13th IEEE International Symposium on Design & Diagnostics of Electronic Circuits and Systems (DDECS 2010), ISBN 978-1-4244-6611-5, pp. 313-316.

• Dominique Gückel. Synthesis of Hardware Simulators for Use in Model Checking. In Dagstuhl 2010. Proceedings of the Joint Workshop of the German Research Training Groups in Computer Science, ISBN 386-130-146-6, p. 76. PDF

• Dominique Gückel, Jörg Brauer, and Stefan Kowalewski. A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification. In Proceedings of 5th IEEE Symposium on Industrial Embedded Systems (SIES 2010), ISBN 978-1-4244-5840-0, pp. 118-127.
• Sebastian Biallas, Jörg Brauer, Dominique Gückel, and Stefan Kowalewski. On-The-Fly Path Reduction. 4th International Workshop on Harnessing Theories for Tool Support in Software (TTSS'10), to appear.
• Thomas Reinbacher, Dominique Gückel, Martin Horauer, and Stefan Kowalewski. Testing Microcontroller Software Simulators. In Proceedings of the Workshop on SLE for CPS at INFORMATIK 2011 (WS4C11), to appear.
• Dominique Gückel and Stefan Kowalewski. Automatic Derivation of Abstract Semantics From Instruction Set Descriptions. In Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011), to appear.

Ich betreue Diplom-/Master- und Bachelor-Arbeiten im Bereich der werkzeuggestützten Entwicklung von Mikrocontroller-Simulatoren sowie im Bereich der Modellierung der Umgebung von Mikrocontrollern. Diese Simulatoren werden im Model-Checking eingesetzt, um den Zustandsraum des Model-Checkers automatisch erzeugen zu können.

Laufende Arbeiten

• Florian Caron: State Partitioning for Model Checking Binary Code (Bachelorarbeit)

Abgeschlossene Arbeiten

• Ivica Bogosavljevic: Synthesizing an Instruction Set Simulator for Model Checking Embedded Systems Software (Masterarbeit)
• Sebastian Wehlmann: Werkzeuggestützte Implementierung eines Simulators für Renesas R8C/Tiny-Mikrocontroller zur Erweiterung des Model-Checkers [mc]square (Diplomarbeit)

Offene Arbeiten

• Werkzeuggestützte Implementierung eines Simulators für 16-Bit-Mikrocontroller (Bachelorarbeit)
• Realisierung von Abstraktionstechniken zum Umgang mit Nichtdeterminismus in synthetisierten Simulatoren
• Erweiterung eines Simulator-Synthese-Frameworks um Unterstützung zur Erzeugung statischer Analysen

Weitere Themen auf Anfrage.

• SS08: Übungsbetreuung zur Vorlesung Formale Methoden für eingebettete Systeme
• SS09: Proseminar Proseminar: Eingebettete Systeme
• WS09/10: Seminar Verifikation und Programmanalyse
• WS10/11: Übungsbetreuung zur Vorlesung Formale Methoden für eingebettete Systeme

Weiterhin beaufsichtige ich regelmäßig Versuche/Prüfungen im Praktikum Hardwarenahe Programmierung (für Studenten im Bachelor-Studiengang Informatik). In der Vergangenheit habe ich zudem solche Versuche/Prüfungen im Praktikum Elektronische Grundlagen für Informatiker beaufsichtigt. Daneben stelle ich Übungs- und ggf. Klausuraufgaben für die Vorlesung Einführung in die Technische Informatik.

• [mc]square
• DFG-Graduiertenkolleg 1298 AlgoSyn