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

Arnd Hartmanns

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

22 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationProceedings Fifth Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2022, Munich, Germany, 2nd April 2022
EditorsClemens Dubslaff, Bas Luttik
Number of pages12
Publication statusPublished - 21 Mar 2022
Event5th Workshop on Models for Formal Analysis of Real Systems 2022 - Munich, Germany
Duration: 2 Apr 20222 Apr 2022
Conference number: 5

Publication series

ISSN (Electronic)2075-2180


Workshop5th Workshop on Models for Formal Analysis of Real Systems 2022


  • 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.

Cite this