logo2.gifdfglogo.gifsponsored project

Validation of Stochastic Systems (VOSS II)


Introducing Voss
Summary of Voss II
Research Aims
TU Dresden Radboud University Nijmegen
Univ of Twente RWTH Aachen
Univ. of the Saarland Univ. der Bundeswehr


VOSS is a research collaboration between the Netherlands and Germany within the NWO-DFG bilateral cooperation program.
On the Dutch side, the participating Universities are the Radboud University Nijmegen and the University of Twente.
The German participating Universities are the RWTH Aachen, the Technical University Dresden, the Saarland University, and the University of the Federal Armed Forces Munich.

As of January 2005, VOSS is in its second phase. For information on the first phase (2001-2004) see the homepage of VOSS I and its
final report.

Summary of the project

The Voss II project aims at the integration of modelling and computer-aided verification techniques for the analysis of complex systems with stochastic behaviour. Rather than proving that systems will always behave correctly, we aim at establishing properties such as "The probability that an airbag will be deployed inadvertently during its operational life is less than 10-9". Our goal is to adapt and extend some prominent techniques that have been successful for modelling and assessing qualitative characteristics of computer systems to a stochastic setting. Modelling formalisms such as input-output automata and process algebra, and verification techniques such as model checking will be thoroughly investigated. We plan to apply these techniques to model, analyse, and optimise systems described as Markov processes, Markov decision processes, and related formalisms.

Research Aims

The joint research activities are focussed on the following four research strands:

Semantic models and equivalences. The goal is to add stochastic features to existing modelling frameworks, such as input-output automata, UML statechart diagrams, or the modelling language of tools such as MoDeST. We wish to develop a uniform framework to reason about non-determinism, concurrency, randomisation and time. We also plan to investigate several notions of testing, process equivalences and other implementation relations, in order to provide these languages with an abstract, well-understood semantics and study the impact of process equivalences as basis for abstraction purposes.

Analysis techniques and tools. For industrial use, it is essential that future tools (a) can handle much bigger systems, and (b) support a richer class of models and properties than the currently available tools. Problem (a) is an especially challenging one, since the number of a system's states typically grows exponentially in the number of components or state variables. This problem will be attacked via two routes, namely symbolic state space representation and abstraction techniques. We study variants of classical multi-terminal binary decision diagrams in order to obtain compact representations of huge Markov models, and develop new methods for the symbolic quantitative analysis. We will develop abstraction techniques for continuous-time Markov decision processes, whose effectiveness will be investigated empirically. In order to advance the state-of-the-art of area (b), the project focuses on temporal logic model checking, where we will develop more expressive temporal logics, being capable of expressing path-based and reward-based properties.

Games and controller synthesis. We address the question of  how to schedule controllable events in a non-deterministic probabilistic setting such that a given specification is fulfilled. This will be perfomed for models with discrete probabilities or stochastic timing (with non-determinism).

Case Studies. The techniques and tools developed in the project will be used to conduct case studies of industrial relevance.


From Nijmegen: Informatics for Technical Applications

From Twente: Formal Methods and Tools

From Twente: Design and Analysis of Communication Systems

From Dresden: Algebraic and Logical Foundations of Computer Science

  • C. Baier
  • T. Blechmann
  • N. Betrand
  • F. Ciesinski
  • M. Groesser
  • J. Klein
  • S. Klüppelholz

From Munich: Design of Computer and Communication Systems

From Aachen: Software Modeling and Verification

From Saarbrücken: Dependable Systems & Software

Project Meetings

24. - 25.01.2005: Saarbrücken/Germany (Agenda)
12. - 13.09.2005: Munich/Germany (Agenda)
12. - 13.01.2006: Twente/Netherland (Agenda)
28. - 29.09.2006: Kerkrade/Netherlands (Agenda)
08. - 09.02.2007: Dresden/Germany (Agenda)
12. - 16.11.2007: Leiden/Netherlands (Agenda, Presentations)

J. Schuster, last modified 11/2007