Research Projects
Table of contents
Current third-party funded projects
RoSI
DFG Research Training Group "Role-based Software Infrastructures for Continuous-Context-Sensitive Systems"
cfaed
Center for Advancing Electronics Dresden
CeTI
Centre for Tactile Internet with Human-in-the-Loop
Foundations of Perspicuous Software Systems
Foundations of Perspicuous Software Systems
Foundations of Perspicuous Software Systems
DFG-Projekt BA-1679/11-1
The project "Modellprüfung für temporale Logiken und gewichtete probabilistische Strukturen" considers theoretical aspects of combining assertions on accumulated weights with temporal logics.
DFG-Projekt BA-1679/12-1
The project "Nicht-Mehrdeutigkeit, Alternierung und Nichtstandardakzeptanz in automatenbasierter Modellprüfung probabilistischer Systeme" considers theoretical and practical aspects of various automata-based approaches to probabilistic model checking for linear temporal logics.
5G Lab Germany
SECAI
School of Embedded Composite Artificial Intelligence
SEMECO
Secure medical microsystems and communications
Former third-party funded projects
SREX
Secure Remote EXecution
IMData
Integrated Hard- and Software Mechanisms for Data-intensive Applications on Heterogeneous Manycore Systems
MEALS
Mobility between Europe and Argentina applying Logics to Systems
QuaOS
The scientific goal of the DFG-project QuaOS was research on methods and models that support the quantitative and functional analysis of properties of Mircokernels.
SYANCO
bilateral DFG-NWO project "Synthesis and analysis of component connectors"
ProbPor II
One main goal of the DFG project "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse II" was the implementation of the model checking tool LiQuor, which is designed for the analysis of reactive probabilistic systems against omega-regular linear-time specifications. Within this scope, research was also done on various theoretical foundations. Amongst others, a probabilistic variant of partial order reduction has been established and the minimization of automata for linear-time specifications has been investigated (see LTL2DSTAR).
ROCKS
The bilateral DFG/NWO project "Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems" focused on modelling and analysis techniques for large scale homogeneous and safety-critical heterogeneous systems.
PROCOPE
DAAD project PROCOPE: academic research collaboration with Dr. Nathalie Bertrand (France)
PROALAR
DAAD project PROALAR: academic research collaboration with Prof. Dr. Pedro D'Argenio (Argentina) (together with Prof. Dr. Holger Hermanns (Universität Saarbrücken))
CREDO
European Union project "Modeling and analysis of evolutionary structures for distributed services"
ProbPor
DFG-project "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse"
VOSS I und VOSS II
The bilateral DFG/NWO-projects "Validation of Stochastic Systems I/II" aimed at the integration of modelling and computer-aided verification techniques for the analysis of complex systems with stochastic behaviour. Within the scope of the projects some prominent modelling and analysis techniques have been adapted and extended to a probabilistic setting and several new methods have been developed.
Veriam
DFG-project "Computerunterstützte Verifikation mit abstrakten Modellen"
DFG-Projekt MA 794/2-1 (und 2-2)
The topic of this project was action refinement in models of reactive systems.
DFG-Projekt MA 794/3-1 (und 3-2)
The topics of this project were specification formalism and the design of verification methods for probabilistic reactive systems.
QuantLA
DFG Research Training Group "Quantitative Logics and Automata"
HAEC
Collaborative Research Centre SFB912 "Highly Adaptive Energy-Efficient Computing"
Tools
ProFeat
A tool for feature-oriented modeling of families of probabilistic systems and their analysis using probabilistic model checking.
LTL2DSTAR
A tool hat converts formulas in linear time logic to deterministic omega-automata, specifically Rabin and Streett automata.
Vereofy
Component based model checking.
JINC
An efficient, easy to use and easily expandable BDD package.