Modest Models and Tools for Real Stochastic Timed Systems

Abstract

We depend on the safe, reliable, and timely operation of cyber-physical systems ranging from smart grids to avionics components. Many of them involve time-dependent behaviours and are subject to randomness. Modelling languages and verification tools thus need to support these quantitative aspects. This paper gives an introduction to quantitative verification using the Modest modelling language and the Modest Toolset. It highlights three recent case studies with increasing demands on model expressiveness and tool capabilities: A case of power supply noise in a network-on-chip modelled as a Markov chain; a case of message routing in satellite constellations that needs Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. For each, we explain the particular conceptual and technical challenges in modelling and verification, and point out open problems for future work.