Forschung
Ich interessiere mich für die Verwendung formaler Methoden in der Information, insbesondere beim Erstellen von sicheren und zuverlässigen Systemen. Dies umfasst Methoden und Werkzeuge zum Design, der Spezifikation, der Validierung und der Verifikation von Soft- und Hardwaresystemen.
Meine Interessen umfassen die drei Bereiche SystemKonstruktion (System Engineering), die Sicherheit und Zuverlässigkeit von Systemen (Safety and Security) und formale Methoden (Formal Methods). Hierbei umfassen meine Interessen sowohl die Grundlagenforschung als auch angewandte Forschungsarbeiten. Deshalb bin ich besonders daran interessiert, Ergebnisse der Grundlagenforschung in industriellen Umgebungen anzuwenden.
Laufende Arbeiten umfassen zum Beispiel die folgenden Bereiche:
-
Spezifikationsbasierte Testverfahren um funktionale und nicht-funktionale (z.B. Testen von Sicherheitseigenschaften) Eigenschaften zu überprüfen
-
Entwicklung formale Semantiken und Beweisumgebungen für objekt-orientierte Systeme
-
Dynamische (DAST), statische (SAST) und kombinierte Verfahren zur Sicherstellung der Sicherheit von Anwendungen.
-
Entwicklung von Verfahren zur Modellierung, Analyse und Ausführung von sicherheits- oder zuvrlässigkeitskritischen Geschäftsprozessen.
-
Flexible Zugriffskontrollverfahren welche den Anforderungen moderner IT Systemen gerecht werden.
top
Aktuelle Arbeiten:
-
Entwicklung von SecureBPMN, einer BPMN Erweiterung welche die Modellierung, Analyse und Ausführung von sicherheitskritischen Geschäftsprozessen erlaubt.
-
Entwicklung von statischen und dynamischen Quellcodeanalyseverfahren zum auffinden von Sicherheitsproblemen in modernen HTML5/JavaScript Anwendungen.
-
Entwicklung von Isabelle/HOL-OCL, einer Beweisumgebung für UML/OCL Spezifikationen. Weitere informationen gibt es auf der HOL-OCL Seite.
-
Entwicklung von HOL-TestGen, einem Test-Daten Generator für den spezifikationsbasierten Unit-Test. Weitere informationen gibt es auf der HOL-TestGen Seite.
-
Entwicklung von Isabelle/OFMC, ein Werkzeug zur Verifikation von Sicherheitsprotokollen welches auf Isabelle/HOL und OFMC aufbaut. Weitere Informationen gibt es auf der Isabelle/OFMC Seite.
-
Bereitstellen von IsaMorph, einer direkt lauffähigen Linux CD mit dem interaktiven Theorembeweiser Isabelle. Weitere informationen gibt es auf der IsaMorph Seite.