Quantitative Verification of Reactive and Embedded Systems

embedded system designs. However, such systems are subject to omnipresent
stochastic influences (failure of components, resource conflicts, signal
perturbations, ... ). Absolute correctness verdicts are therefore often
unrealistic. Instead, the analysis of such system designs must allow one to
establish correctness up to a quantifiable notion of uncertainty.

This talk discusses concepts, algorithms, and tools that enable the
quantification of correctness, performance, and dependability properties of
reactive and embedded systems. The main focus will be on techniques supported
by modern, high-level specification languages. This research strand has the
potential to close a disturbing gap between traditional performance evaluation
and computer aided verification approaches.

The talk will first sketch how performance and dependability models can be
derived from high-level specification languages. Then it will be discussed in
detail how computer aided verification techniques ("model checking") can be
applied to those models in order to quantify performance and dependability
properties, but also correctness properties. The practicability of this
approach will be demonstrated by means of prototypical software tools. The talk
concludes by outlining the scientific perspective of this research.