Research
Links to our current research projects
- 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.
Links to 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