Links to our current research projects
Directed Model Checking in the Analysis of Reactive and Probabilistic Systems.
- Real-Time Systems
Heuristic Search and Abstract Model Checking for Real-Time Systems.
Formal Verification of Availability Properties.
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