> Quantitative Verification beyond Markov: Models, Techniques and Tools

Abstract:
> Proper consideration of quantitative aspects is crucial to formally
> model and analyse many complex critical systems. We need to properly
> represent randomised and real-time behaviour in models, and we want to
> compute quantitative measures like the worst-case probability of
> failure during system lifetime or the expected energy consumption over
> time. In this talk, I will present stochastic timed automata (STA) as
> a suitable and flexible formal model for this purpose. Many well-known
> Markovian and real-time models, for example MDP, GSMP and timed
> automata, are special cases of STA. I will give an overview of the
> basic model checking approach for STA and highlight recent advances in
> dealing with large models and bounded properties. I will demonstrate
> the Modest Toolset, a modular multiple-formalism, multiple-solution
> implementation that supports STA-based modelling and analysis, before
> concluding with an outlook on stochastic hybrid systems.