Research

Our current research projects

• CausCheck 
  Causality Checking for Complex System Models

• QuantUM 
  Safety Analysis of Complex Sytem and Software Architectures 

• DiRePro
  Directed Model Checking in the Analysis of Reactive and Probabilistic Systems.
  • Real-Time Systems
    Heuristic Search and Abstract Model Checking for Real-Time Systems.
  • Probabilistic Systems
    Formal Verification of Availability Properties.

• IMCOS
  Incomplete Model Checking for Concurrent Object-oriented Systems.

• Directed Model Checking
  We investigate the use of directed search algorithms in explicit state model checking.

Our past research projects

• VIP - A Visual Interface for Promela
  The objective of this research was to reconcile Promela with state-of-the-art visual modeling techniques for real-time systems, in particular UML-RT, and to provide suitable tool support.

• Visual Modeling and Formal Validation
  This presents a collection of papers pertaining to the v-Promela notation and the VIP (Visual Interface for Promela) tool.

• Formal Modeling and Validation of Distributed, Object-Oriented Systems
  This compendium presents articles on case studies in the modeling of distributed, object-oriented systems, using various modeling languages and tools.

• Message Sequence Charts and Message Flow Graphs

• Efficient, Parallel Protocol Implementation

• SDL, Real-Time and Quality of Service

Links to research programs that we are involved in

• Member in the PhD Program (Graduiertenkolleg) Explorative Analysis and Visualization of Large Information Spaces

• Associate Member in the Transregional Collaborative Research Center (Sonderforschungsbereich) 14 Automated Verifcation and Analysis of Complex Systems (AVACS)