  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. In my
invited presentation at MARS 2022, I gave an introduction to quantitative
verification using the Modest modelling language and the Modest Toolset, and
highlighted 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 uses Markov decision processes with distributed
information; and a case of optimising an attack on Bitcoin via Markov automata
model checking. This paper summarises the presentation.
