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.