Forschung

Arbeitsgebiete:

Mathematische Methoden für Spezifikation, Entwurf, Validierung komplexer informationstechnischer Systeme, insbesondere für physikalisch verteilte und nebenläufig operierende Anwendungen

Zentrale Fragestellungen:

• Synchronisationsmechanismen
• Übergang zwischen Synchronie und Asynchronie
• Abstraktion und Verfeinerung
• Constraints und Kompositionalitätsproblem
• Semantik modellorientierter Entwurfssprachen (UML, Statecharts)

Mathematische Grundlagen:  

Intuitionistische und modale Logiken, Lax Logic, Kripke Semantiken, Heytingalgebra, Typentheorie, Prozessalgebren

Anwendungsfelder:

Eingebettete und interaktive Systeme, Web-basierte Dienste, verteilte Transaktionssysteme, Sicherheitsprotokolle, mobile intelligente Agenten, Verteilte Geschäftsprozesse, komponentenbasiertes Programmieren

Automatische und interaktive Validierungsverfahren:

Modellprüfung, Verzögerungsanalyse, Typprüfung, Theorembeweisen

Forschungsprojekte

• REALTYPE – Type Analysis for Component-based Real-time Programming (EPSRC 2001-2003) 
• LAX LOGIC – Lax Logic applied to Formal System Design (EPSRC 1999-2002) 
• TYPES-Mitglied der EU Types Working Group (IST-EU-29001, 2001-2008) 
• SPACMODL – Semantic Processing and Auditing in Constructive Modal Logic (DFG-Projekt,  2008 - 2012)
• PRETSY – Precision Timed Synchronous Reactive Processing (DFG-Projekt, Beginn 2012)