Is it a good idea to ride a bike with a wireless brake ? How to dimension buffer sizes in a NoC ? What availability can be expected for Gallileo IOV ? Might photovoltaic overproduction blow out the European electricity network ? Maybe. Maybe not. Probably ? The era of power-aware, wireless and distributed systems of systems asks for strong quantitative answers to such questions.

This talk introduces a promising attack on this challenge. The approach merges two well-established strands of informatics research and practice : verification of concurrent systems and performance evaluation. Instead of guaranteeing that a system is performing the expected tasks, we are ultimately interested in guaranteeing that the system performs its task within a given time bound and with (energy) costs within a given limit. Or better : that the probability thereof is above a given threshold. This presentation paints the landscape of behavioural models for probability, time, and cost, with a mild focus onconcurrent Markov models and process calculi. It discusses foundational aspects of compositional modelling and model checking such systems, and show how these techniques are applied in different real-life cases.