An Overview of Modest Models and Tools for Real Stochastic Timed Systems

Arnd Hartmanns

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.

Invited Presentation in Clemens Dubslaff and Bas Luttik: Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems (MARS 2022), Munich, Germany, 2nd April 2022, Electronic Proceedings in Theoretical Computer Science 355, pp. 1–12.
Published: 21st March 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: