Hier werden die Unterschiede zwischen zwei Versionen angezeigt.
| Beide Seiten der vorigen Revision Vorhergehende Überarbeitung Nächste Überarbeitung | Vorhergehende Überarbeitung Letzte Überarbeitung Beide Seiten der Revision | ||
|
lehrstuhl:mitarbeiter:schlich [2009/08/07 11:40] schlich |
lehrstuhl:mitarbeiter:schlich [2011/11/03 12:55] kux gelöscht |
||
|---|---|---|---|
| Zeile 1: | Zeile 1: | ||
| ====== Dr.rer.nat. Bastian Schlich ====== | ====== Dr.rer.nat. Bastian Schlich ====== | ||
| \\ | \\ | ||
| + | {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}}\\ | ||
| + | \\ | ||
| + | schlich[at]embedded[dot]rwth-aachen[dot]de\\ | ||
| + | |||
| /* | /* | ||
| {| | {| | ||
| Zeile 6: | Zeile 10: | ||
| || {{:lehrstuhl:mitarbeiter:schlich.jpg|}} | || {{:lehrstuhl:mitarbeiter:schlich.jpg|}} | ||
| || | || | ||
| + | |||
| Post-Doktorand\\ | Post-Doktorand\\ | ||
| Gruppenleiter der Gruppe Formale Verifikation\\ | Gruppenleiter der Gruppe Formale Verifikation\\ | ||
| Zeile 18: | Zeile 23: | ||
| Addresse: Ahornstr. 55, 52074 Aachen | Addresse: Ahornstr. 55, 52074 Aachen | ||
| |} | |} | ||
| - | */ | ||
| {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}}\\ | {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}}\\ | ||
| \\ | \\ | ||
| Zeile 25: | Zeile 29: | ||
| \\ | \\ | ||
| Wenn ich eine Email nicht innerhalb einer vertretbaren Zeit beantworte, melden Sie sich bitte telefonisch bei mir. Es kann sein, dass Ihre Email automatisch von unserem Spam-Filter gelöscht wurde.\\ | Wenn ich eine Email nicht innerhalb einer vertretbaren Zeit beantworte, melden Sie sich bitte telefonisch bei mir. Es kann sein, dass Ihre Email automatisch von unserem Spam-Filter gelöscht wurde.\\ | ||
| + | \\ | ||
| + | Sprechstunde: Dienstags 13:00 - 14:00 (bitte Termin per Email vereinbaren)\\ | ||
| \\ | \\ | ||
| Email: schlich[at]embedded[dot]rwth-aachen[dot]de\\ | Email: schlich[at]embedded[dot]rwth-aachen[dot]de\\ | ||
| Zeile 34: | Zeile 40: | ||
| \\ | \\ | ||
| - | /*===== Neuigkeiten ===== | + | ===== Neuigkeiten ===== |
| - | Ich bin vom 03.07. bis zum 13.07.2009 im Urlaub. In dringenden Fällen können Sie Herrn [[:lehrstuhl:mitarbeiter:kamin|Kamin]] kontaktieren. | + | Ich bin bis zum 13.09.2009 im Urlaub. In dringenden Fällen können Sie Herrn [[:lehrstuhl:mitarbeiter:brauer|Brauer]] kontaktieren. |
| */ | */ | ||
| ===== Persönlich ===== | ===== Persönlich ===== | ||
| - | Seit Juli 2008 bin ich Post-Doktorand am Lehrstuhl Informatik 11 (Software für eingebettete Systeme). An diesem Lehrstuhl leite ich die Gruppe Formale Verifikation. Mein Forschungsschwerpunkt ist die formale Verifikation von Software für eingebettete Systeme. Unter formaler Verifikation verstehe ich die Anwendung von Methoden wie z. B. statische Analyse, abstrakte Interpretation und Model-Checking.\\ | + | Ich war von April 2004 bis Februar 2010 erst als Doktorand und danach als Postdoc am Lehrstuhl Informatik 11 (Software für eingebettete Systeme) beschäftigt. An diesem Lehrstuhl leitete ich die Gruppe Formale Verifikation. Mein Forschungsschwerpunkt war die formale Verifikation von Software für eingebettete Systeme. Unter formaler Verifikation verstehe ich die Anwendung von Methoden wie z. B. statische Analyse, abstrakte Interpretation und Model-Checking.\\ |
| \\ | \\ | ||
| - | In der Gruppe arbeiten wir an einem Werkzeug zur Analyse von Assembler-Code für Mikrocontroller und AWL-Programmen für SPSen. Das Werkzeug heißt [[http://www.embedded.rwth-aachen.de/mc_square|[mc]square]]. In diesem Werkezug kombinieren wir unterschiedliche formale Methoden und passen sie an die Gegebenheiten von eingebetteten Systemen an. Das Hauptaugenmerk hierbei liegt auf der Anwendung theoretischer Resultate auf reale Probleme. Das Werkzeug soll möglichst leicht zu benutzen sein und keine Änderungen an den zu verifizierenden Programmen benötigen.\\ | + | Die Gruppe arbeitet an einem Werkzeug zur Analyse von Assembler-Code für Mikrocontroller und AWL-Programmen für SPSen. Das Werkzeug heißt [[http://www.embedded.rwth-aachen.de/mc_square|[mc]square]]. In diesem Werkezug werden unterschiedliche formale Methoden kombiniert und an die Gegebenheiten von eingebetteten Systemen angepasst. Das Hauptaugenmerk hierbei liegt auf der Anwendung theoretischer Resultate auf reale Probleme. Das Werkzeug soll möglichst leicht zu benutzen sein und keine Änderungen an den zu verifizierenden Programmen benötigen.\\ |
| \\ | \\ | ||
| - | In einem weiteren Projekt entwickeln wir ein Werkezug für die statische Analyse von C Code, welches die Entwicklung von eingebetteter Software anhand des bevorstehenden ISO Standards ISO 26262 unterstützen soll. Wir werden zuerst ein Plugin für die Eclipse Entwicklungsumgebung erstellen. Später werden wir auch ein Plugin für die Microsoft Visual Studio Entwicklungsumgebung implementieren.\\ | + | In einem weiteren Projekt wird ein Werkezug für die statische Analyse von C Code entwickelt, welches die Entwicklung von eingebetteter Software anhand des bevorstehenden ISO Standards ISO 26262 unterstützen soll. Es wird zuerst ein Plugin für die Eclipse Entwicklungsumgebung erstellt. Später wird auch ein Plugin für die Microsoft Visual Studio Entwicklungsumgebung implementiert.\\ |
| \\ | \\ | ||
| Meinen Doktortitel habe ich im Juni 2008 von der RWTH Aachen erhalten. Der Titel meiner Dissertation lautet "Model Checking of Software for Microcontrollers". Meine Diplomarbeit habe ich am Lehrstuhl für Software-Technologie der Universität Dortmund geschrieben. Der Titel meiner Diplomarbeit ist "Konzeption und Realisierung eines Werkzeugs zur Unterstützung der Test-Driven-Developments".\\ | Meinen Doktortitel habe ich im Juni 2008 von der RWTH Aachen erhalten. Der Titel meiner Dissertation lautet "Model Checking of Software for Microcontrollers". Meine Diplomarbeit habe ich am Lehrstuhl für Software-Technologie der Universität Dortmund geschrieben. Der Titel meiner Diplomarbeit ist "Konzeption und Realisierung eines Werkzeugs zur Unterstützung der Test-Driven-Developments".\\ | ||
| - | ===== Forschungsinteressen ===== | ||
| - | * Formale Methoden | ||
| - | * Software Model-Checking | ||
| - | * Statische Analyse | ||
| - | * Abstrakte Interpretation | ||
| - | * Eingebettete Software | ||
| - | * Assembler-Code | ||
| - | * C-Code | ||
| - | * Mikrocontroller | ||
| - | * Speicherprogrammierbare Steuerungen | ||
| ===== Publikationen ===== | ===== Publikationen ===== | ||
| Zeile 68: | Zeile 64: | ||
| ==== Bachelor-, Master- und Diplomarbeiten ==== | ==== Bachelor-, Master- und Diplomarbeiten ==== | ||
| - | Wer Interesse hat, eine Abschlussarbeit im Bereich von [mc]square zu schreiben, kann sich gerne bei mir melden oder die Themen ansehen die [[:lehre:abschlussarbeiten|hier]] beschrieben sind. | + | * Gegenbeispiel-geleitete Abstraktionsverfeinerung für speicherprogrammierbare Steuerungen (Sebastian Biallas) |
| - | + | * [[:lehre:abschlussarbeiten:DAVK005]] (Michael Lambertz) | |
| - | === Laufend === | + | * Statische Analyse für den Renesas R8C/23 Mikrocontroller (Jörg Toborg) |
| - | + | * Statische Analyse von Mikrocontrollerprogrammen mittels SAT- und Constraint-Solving (Lucas Brutschy) | |
| - | === Abgeschlossen === | + | * [[:lehre:abschlussarbeiten:implementierung_eines_simulators_fuer_renesas]] (Mudassir Rasool) |
| + | * [[:lehre:abschlussarbeiten:synthesizing_is_simulators_for_model_checking_es_software]] (Ivica Bogosavljevic) | ||
| * [[:lehre:abschlussarbeiten:model_checking_von_anweisungslisten-prgrammen_fuer_speicherprogrammierbare_steuerung_mit_hilfe_von_mc_square]] (Jörg Wernerus) | * [[:lehre:abschlussarbeiten:model_checking_von_anweisungslisten-prgrammen_fuer_speicherprogrammierbare_steuerung_mit_hilfe_von_mc_square]] (Jörg Wernerus) | ||
| * [[:lehre:abschlussarbeiten:parallelisierung_in_mcsquare]] (Stefan Mau) | * [[:lehre:abschlussarbeiten:parallelisierung_in_mcsquare]] (Stefan Mau) | ||