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/06/12 20:08] brauer |
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 ====== | ||
| - | ~~NOTOC~~ | ||
| \\ | \\ | ||
| + | {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}}\\ | ||
| + | \\ | ||
| + | schlich[at]embedded[dot]rwth-aachen[dot]de\\ | ||
| + | |||
| + | /* | ||
| {| | {| | ||
| |- | |- | ||
| || {{:lehrstuhl:mitarbeiter:schlich.jpg|}} | || {{:lehrstuhl:mitarbeiter:schlich.jpg|}} | ||
| || | || | ||
| - | Research Assistant\\ | + | |
| - | schlich[at]embedded[dot]rwth-aachen[dot]de\\ | + | Post-Doktorand\\ |
| + | Gruppenleiter der Gruppe Formale Verifikation\\ | ||
| \\ | \\ | ||
| - | If I do not answer an email within reasonable time, please give me a call because your email might be removed by our spam filter.\\ | + | 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.\\ |
| \\ | \\ | ||
| - | Phone +49 241 80 21158\\ | + | Email: schlich[at]embedded[dot]rwth-aachen[dot]de\\ |
| - | Fax +49 241 80 6 21158\\ | + | Telefon: +49 241 80 21158\\ |
| + | Fax: +49 241 80 6 21158\\ | ||
| \\ | \\ | ||
| - | Address: Ahornstr. 55, 52074 Aachen, Germany\\ | + | Büro: Raum 2325 (Gebäude H)\\ |
| - | Office: room 2325 (Building H) | + | Addresse: Ahornstr. 55, 52074 Aachen |
| |} | |} | ||
| + | {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}}\\ | ||
| + | \\ | ||
| + | Post-Doktorand\\ | ||
| + | Gruppenleiter der Gruppe Formale Verifikation\\ | ||
| + | \\ | ||
| + | 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\\ | ||
| + | Telefon: +49 241 80 21158\\ | ||
| + | Fax: +49 241 80 6 21158\\ | ||
| + | \\ | ||
| + | Büro: Raum 2325 (Gebäude H)\\ | ||
| + | Addresse: Ahornstr. 55, 52074 Aachen | ||
| + | |||
| + | \\ | ||
| + | ===== Neuigkeiten ===== | ||
| + | |||
| + | Ich bin bis zum 13.09.2009 im Urlaub. In dringenden Fällen können Sie Herrn [[:lehrstuhl:mitarbeiter:brauer|Brauer]] kontaktieren. | ||
| + | */ | ||
| + | |||
| + | ===== Persönlich ===== | ||
| + | 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.\\ | ||
| \\ | \\ | ||
| - | === Personal === | + | 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.\\ |
| - | I am a research assistant at the embedded software laboratory since April 2004. My research topic is the formal verification of software for embedded systems.\\ | + | |
| \\ | \\ | ||
| - | At present I am working on a model checker for microcontroller code. It is called [mc]square. The main focus is the application of theoretical results to real problems. The model checker should be as user-friendly as possible and the need for manual preparation of the code should be as small as possible. In the tool, we combine different formal methods such as model checking, abstract interpretation, and static analysis.\\ | + | 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.\\ |
| \\ | \\ | ||
| - | I received my Doctoral degree in June 2008 from the RWTH Aachen University. The title of my Dissertation thesis is "Model Checking of Software for Microcontollers". I wrote my Diploma thesis at the chair of Software-Technology, University of Dortmund. The topic of the thesis is "Konzeption und Realisierung eines Werkzeugs zur Unterstützung des 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".\\ |
| - | ===== Research Interests ===== | ||
| - | * formal verification | ||
| - | * software model checking | ||
| - | * model checking of assembly code | ||
| - | * software for embedded systems | ||
| - | * software for microcontrollers | ||
| - | ===== Publications ===== | + | ===== Publikationen ===== |
| ~~NOCACHE~~ | ~~NOCACHE~~ | ||
| <BIBTEX: file=publikationen style=I11 sort=year filter=schlich> | <BIBTEX: file=publikationen style=I11 sort=year filter=schlich> | ||
| - | ===== BSc/MSc/Diploma Theses ===== | + | ===== Lehre ===== |
| - | ==== Ongoing ==== | + | ==== Bachelor-, Master- und Diplomarbeiten ==== |
| - | ==== Finished ==== | + | * Gegenbeispiel-geleitete Abstraktionsverfeinerung für speicherprogrammierbare Steuerungen (Sebastian Biallas) |
| - | + | * [[:lehre:abschlussarbeiten:DAVK005]] (Michael Lambertz) | |
| - | * Parallel and Distributed Construction of the State Spaces in the Model Checker [mc]square - Stefan Mau | + | * Statische Analyse für den Renesas R8C/23 Mikrocontroller (Jörg Toborg) |
| - | * Model Checking of Instruction List Programs for Programmable Logik Controllers using [mc]square - Jörg Wernerus | + | * Statische Analyse von Mikrocontrollerprogrammen mittels SAT- und Constraint-Solving (Lucas Brutschy) |
| - | * Extending the symbolic representation of states in [mc]square - [[:lehrstuhl:mitarbeiter:kamin]] | + | * [[:lehre:abschlussarbeiten:implementierung_eines_simulators_fuer_renesas]] (Mudassir Rasool) |
| - | * Model Checking of Sensor Network Nodes with [mc]square - Matthias Moers | + | * [[:lehre:abschlussarbeiten:synthesizing_is_simulators_for_model_checking_es_software]] (Ivica Bogosavljevic) |
| - | * Extending the Model Checker [mc]square by User-Defined Environments - [[:lehrstuhl:mitarbeiter:gueckel]] | + | * [[:lehre:abschlussarbeiten:model_checking_von_anweisungslisten-prgrammen_fuer_speicherprogrammierbare_steuerung_mit_hilfe_von_mc_square]] (Jörg Wernerus) |
| - | * Extending the model checking tool [mc]square to handle the Infineon XC167 microcontroller - Florian Scheuer | + | * [[:lehre:abschlussarbeiten:parallelisierung_in_mcsquare]] (Stefan Mau) |
| - | * Application of Static Analysis in the Field of Model Checking Software for Embedded Systems - Jann Löll | + | * [[:lehre:abschlussarbeiten:erweiterung_der_symbolischen_zustandsdarstellung_in_mc_square]] ([[:lehrstuhl:mitarbeiter:kamin]]) |
| - | * Symbolic Model Checking of Assembly Code in [mc]square - [[:lehrstuhl:mitarbeiter:schommer]] | + | * [[:lehre:abschlussarbeiten:model_checking_von_sensornetzwerk-knoten_mit_hilfe_von_mc_square]] (Matthias Moers) |
| - | * An Approach for Model Checking Embedded Systems Software - Michael Rohrbach | + | * [[:lehre:abschlussarbeiten:erweiterung_des_model-checkers_mc_square_um_benutzerdefinierte_umgebungen]] ([[:lehrstuhl:mitarbeiter:gueckel]]) |
| - | * Analysis of Application Potential of Formal Verification in the Field of Engine Control Software - [[:lehrstuhl:mitarbeiter:polzer]] | + | * [[:lehre:abschlussarbeiten:erweiterung_des_model-checkers_mc_square_fuer_den_infineon_xc167_mikcrocontroller]] (Florian Scheuer) |
| - | * Requirements for a model checker for MATLAB/Simulink - [[:lehrstuhl:mitarbeiter:palczynski]] | + | * [[:lehre:abschlussarbeiten:einsatz_von_statischen_analysen_im_bereich_des_model-checking_von_software_fuer_eingebettete_systeme]] (Jann Löll) |
| + | * [[:lehre:abschlussarbeiten:symbolisches_model-checking_mit_mc_square]] ([[:lehrstuhl:mitarbeiter:schommer]]) | ||
| + | * [[:lehre:abschlussarbeiten:ein_ansatz_zum_model-checking_von_Software_fuer_eingebettete_systeme]] (Michael Rohrbach) | ||
| + | * [[:lehre:abschlussarbeiten:untersuchungen_zum_anwendungspotential_der_formalen_verifikation]] ([[:lehrstuhl:mitarbeiter:polzer]]) | ||
| + | * [[:lehre:abschlussarbeiten:model_checking_von_matlab_simulink_modellen]] ([[:lehrstuhl:mitarbeiter:palczynski]]) | ||
| - | ===== Teaching ===== | + | ==== Vorlesungen und Seminare ==== |
| - | * Winter semester 09/10: [[:lehre:wise0910:formale_methoden]] (Lecture) | + | * Wintersemester 09/10: [[:lehre:wise0910:formale_methoden]] (Vorlesung) |
| - | * Summer semester 09: [[http://www-i2.informatik.rwth-aachen.de/i2/teaching/|Applying Formal Verification Methods to Embedded Systems]] (Seminar) | + | * Sommersemester 09: [[http://www-i2.informatik.rwth-aachen.de/i2/teaching/|Anwendung formaler Verifikationsmethoden auf eingebettete Systeme]] (Seminar) |
| - | * Winter semester 08/09: [[:lehre:wise0809:seminar_statische_analyse]] (Seminar) | + | * Wintersemester 08/09: [[:lehre:wise0809:seminar_statische_analyse]] (Seminar) |
| - | * Summer semester 08: [[:lehre:sose08:formale_methoden]] (Lecture) | + | * Sommersemester 08: [[:lehre:sose08:formale_methoden]] (Vorlesung) |
| - | * Summer semester 07: [[:lehre:sose07:formale_methoden]] (Lecture) | + | * Sommersemester 07: [[:lehre:sose07:formale_methoden]] (Vorlesung) |
| - | * Winter semester 06/07: [[:lehre:wise0607:testen_von_eingebetteten_systemen]] (Seminar) | + | * Wintersemester 06/07: [[:lehre:wise0607:testen_von_eingebetteten_systemen]] (Seminar) |
| - | * Summer semester 06: Software Award 2006 | + | * Sommersemester 06: [[:lehre:sose06:software_award]] |
| - | * Winter semester 05/06: [[:lehre:wise0506:systematische_software_entwicklung]] (Lecture) | + | * Wintersemester 05/06: [[:lehre:wise0506:systematische_software_entwicklung]] (Vorlesung) |
| - | * Summer semester 05: [[:lehre:sose05:formale_methoden]] (Lecture) | + | * Sommersemester 05: [[:lehre:sose05:formale_methoden]] (Vorlesung) |
| - | * Winter semester 04/05: Systems Programming (Lecture) | + | * Wintersemester 04/05: Systemprogrammierung (Vorlesung) |
| - | * Winter semester 04/05: Application of Model Checking to Embedded Systems (Seminar) | + | * Wintersemester 04/05: Anwendung von Model-Checking auf eingebettete Systeme (Seminar) |
| - | * Summer semester 04: Hybrid and Real-Time Systems (Seminar) | + | * Sommersemester 04: Hybride und Echtzeitsysteme (Seminar) |