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

Arnd Hartmanns

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

3 Downloads (Pure)

Abstract

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
Pages1-12
Number of pages12
DOIs
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

NameEPTCS
Volume355

Workshop

Workshop5th Workshop on Models for Formal Analysis of Real Systems 2022
Country/TerritoryGermany
CityMunich
Period2/04/222/04/22

Fingerprint

Dive into the research topics of 'An Overview of Modest Models and Tools for Real Stochastic Timed Systems'. Together they form a unique fingerprint.

Cite this