Forschungsprojekte

Aktuelle Drittmittelprojekte des Lehrstuhls

RoSI

DFG Research Training Group "Rollenbasierte Software-Infrastrukturen"

cfaed

Center for Advancing Electronics Dresden

CeTI

Centre for Tactile Internet with Human-in-the-Loop

Foundations of Perspicuous Software Systems

DFG-Projekt BA-1679/11-1

Das Projekt "Modellprüfung für temporale Logiken und gewichtete probabilistische Strukturen" untersucht theoretische Aspekte der Verknüpfung von Bedingungen an akkumulierte Gewichte mit temporalen Logiken.

DFG-Projekt BA-1679/12-1

Das Projekt "Nicht-Mehrdeutigkeit, Alternierung und Nichtstandardakzeptanz in automatenbasierter Modellprüfung probabilistischer Systeme" untersucht theoretische und praktische Aspekte von verschiedenen automaten-basierten Ansätzen für probabilistisches Model Checking für lineare temporale Logiken.

5G Lab Germany

SECAI

School of Embedded Composite Artificial Intelligence

SEMECO

Secure medical microsystems and communications

Abgeschlossene Drittmittelprojekte

SREX

Secure Remote EXecution

IMData

Integrierte Hard- and Software Mechanismen für datenintensive Anwendungen auf Heterogenen Mehrkernsystemen

MEALS

Mobility between Europe and Argentina applying Logics to Systems

QuaOS

Das Ziel des DFG-Projektes QuaOS war 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" war 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 wurden auch verschiedene theoretische Grundlagen erforscht. Dies umfasste 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" war es, Modellierungs- und Analysetechniken für large-scale homogene und sicherheitskritische heterogene stochastische Systeme zu entwickeln.

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"

VOSS I und VOSS II

VOSS II VOSS I

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.

QuantLA

DFG Graduiertenkolleg "Quantitative Logics and Automata"

HAEC

SFB912 "Highly Adaptive Energy-Efficient Computing"

Tools

ProFeat

Ein Werkzeug zur feature-orientierten Modellierung von Familien von probabilistischen Systemen und deren Analyse mittels probabilistischem Model Checking.

LTL2DSTAR

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

Vereofy

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

JINC

Ein effizientes, erweiterbares und objektorientiertes BDD-Paket.