Oct 27, 2015: Arnd Hartmanns: Models, Tools and Techniques for Stochastic Timed Systems

October 27, 2015Models, Tools and Techniques for Stochastic Timed Systems
Room: HB 2AArnd Hartmanns

Proper consideration of quantitative aspects is crucial to formally model and analyse many complex critical systems. Timeouts and randomised algorithms as well as disturbances such as random failures and delays need to be modelled. The probability of desired behaviour, the expected time to success, or the average number of errors over time need to be analysed. These are aspects of stochastic timed systems: Nondeterminism, real time, probabilistic decisions, and any combination thereof. In this talk, I will present stochastic timed automata (STA) as a suitable and flexible model. Many well-known Markovian and real-time models, for example MDPs and timed automata, are special cases of STA. I will give an overview of the state of the art in exhaustive and statistical model checking to analyse these submodels. I will demonstrate the Modest Toolset, which implements a modular multiple-formalism, multiple-solution approach to model and analyse STA.