Aktuelle Drittmittelprojekte des Lehrstuhls:

QuantLA

DFG Graduiertenkolleg "Quantitative Logics and Automata"

HAEC

SFB912 "Highly Adaptive Energy-Efficient Computing"

QuaOS

Das Ziel des DFG-Projektes QuaOS ist die Erforschung neuer Methoden und mathematischer Modelle zur Analyse quantitativer und funktionaler Eigenschaften von Mikrokernen.

SYANCO

bilaterales DFG-NWO Projekt "Synthesis and analysis of component connectors"

ProbPor II

Eines der Hauptziele des DFG-Projekts "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse II" ist die Erstellung des Model Checking-Tools LiQuor, mit dem sich reaktive probabilistische Systeme hinsichtlich omega-regulärer und temporallogischer Spezifikationen analysieren lassen. In diesem Rahmen werden auch verschiedene theoretische Grundlagen erforscht. Dies umfasst unter anderem eine probabilistische Variante der Partial Order Reduction sowie Minimierungsalgorithmen für Automatendarstellungen temporallogischer Eigenschaften (siehe auch LTL2DSTAR).

ROCKS

Hauptziel des bilateralen DFG/NWO Projekt "Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems" ist es, Modellierungs- und Analysetechniken für large-scale homogene und sicherheitskritische heterogene stochastische Systeme zu entwickeln.

---

Abgeschlossene Drittmittelprojekte:

PROCOPE

DAAD Projekt PROCOPE: Programm des projektbezogenen Personenaustauschs mit Dr. Nathalie Bertrand (Frankreich)

PROALAR

DAAD Projekt PROALAR: Programm des projektbezogenen Personenaustauschs mit Prof. Dr. Pedro D'Argenio (Argentinien) (zusammen mit Prof. Dr. Holger Hermanns (Universität Saarbrücken))

CREDO

EU Projekt "Modeling and analysis of evolutionary structures for distributed services"

ProbPor

DFG-Projekt "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse": siehe ProbPor II unter aktuelle Projekte

VOSS I und VOSS II

Ziel der bilateralen DFG/NWO-Projekte "Validation of Stochastic Systems I/II" war die Verflechtung der Modellierung und der automatischen Analyse komplexer stochastischer Systeme. Im Rahmen der beiden Projekte wurden nicht nur viele erfolgreiche bestehende Modelle und Analysetechniken um stochastische Komponenten erweitert und angepasst, sondern auch einige neue Methoden entwickelt.

Veriam

DFG-Projekt "Computerunterstützte Verifikation mit abstrakten Modellen"

DFG-Projekt MA 794/2-1 (und 2-2)

Thema des Projekts war die Aktionsverfeinerung in Modellen reaktiver Systeme.

DFG-Projekt MA 794/3-1 (und 3-2)

Thema des Projekts waren Spezifikations-Formalismen und der Entwurf von Verifikationsmethoden für probabilistische reaktive Systeme.

---

Tools:

LTL2DSTAR

ein Werkzeug zur Erstellung von deterministischen Rabin/Streett-Automaten aus gegebenen LTL-Formeln

LiQuor

ein Werkzeug zur Analyse von Markov Entscheidungsprozessen gegen Linearzeit-Spezifikationen

Reo Model Checking Tools

Dieses Projekt beschäftigt sich mit Model Checking von komponentenbasierten Systemen.

JINC

ein effizientes, erweiterbares und objektorientiertes BDD-Paket.