sponsored project
Validation of Stochastic Systems (VOSS II)
|
Contents
of Site
|
|
|
|
sponsored project|
Contents
of Site
|
|
|
|
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.
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.
24. - 25.01.2005: Saarbrücken/Germany (Agenda)
12. - 13.09.2005: Munich/Germany (Agenda)
12. - 13.01.2006: Twente/Netherlands (Agenda)
28. - 29.09.2006: Kerkrade/Netherland (Agenda)
08. - 09.02.2007: Dresden/Germany (Agenda)
12. - 16.11.2007: Leiden/Netherlands
