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.
|Title of host publication||Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2022, Munich, Germany, 2nd April 2022|
|Editors||Clemens Dubslaff, Bas Luttik|
|Number of pages||12|
|Publication status||Published - 21 Mar 2022|
|Event||5th Workshop on Models for Formal Analysis of Real Systems 2022 - Munich, Germany|
Duration: 2 Apr 2022 → 2 Apr 2022
Conference number: 5
|Workshop||5th Workshop on Models for Formal Analysis of Real Systems 2022|
|Period||2/04/22 → 2/04/22|
- This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.