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

Arnd Hartmanns

doi:10.4204/EPTCS.355.1

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

Arnd Hartmanns

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

52 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 language	English
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
Pages	1-12
Number of pages	12
DOIs	https://doi.org/10.4204/EPTCS.355.1
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

Publication series

Name	EPTCS
Volume	355
ISSN (Electronic)	2075-2180

Workshop

Workshop	5th Workshop on Models for Formal Analysis of Real Systems 2022
Country/Territory	Germany
City	Munich
Period	2/04/22 → 2/04/22

Keywords

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.

Access to Document

10.4204/EPTCS.355.1Licence: CC BY

ArticleFinal published version, 224 KBLicence: CC BY

Cite this

@inproceedings{96c9bb2cb8f34948ac5633d101904caf,

title = "An Overview of Modest Models and Tools for Real Stochastic Timed Systems",

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.",

keywords = "This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union{\textquoteright}s Horizon 2020 research and innovation programme under Marie Sk{\l}odowska-Curie Actions grant number 101008233.",

author = "Arnd Hartmanns",

note = "Funding Information: ∗The author was supported by NWO VENI grant no. 639.021.754 and by the European Union{\textquoteright}s Horizon 2020 research and innovation programme under the Marie Sk{\l}odowska-Curie grant agreement No. 101008233. Publisher Copyright: {\textcopyright} A. Hartmanns; 5th Workshop on Models for Formal Analysis of Real Systems 2022 ; Conference date: 02-04-2022 Through 02-04-2022",

year = "2022",

month = mar,

day = "21",

doi = "10.4204/EPTCS.355.1",

language = "English",

series = "EPTCS",

pages = "1--12",

editor = "Clemens Dubslaff and Bas Luttik",

booktitle = "Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2022, Munich, Germany, 2nd April 2022",

}

Hartmanns, A 2022, An Overview of Modest Models and Tools for Real Stochastic Timed Systems. in C Dubslaff & B Luttik (eds), Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2022, Munich, Germany, 2nd April 2022. EPTCS, vol. 355, pp. 1-12, 5th Workshop on Models for Formal Analysis of Real Systems 2022, Munich, Germany, 2/04/22. https://doi.org/10.4204/EPTCS.355.1

An Overview of Modest Models and Tools for Real Stochastic Timed Systems. / Hartmanns, Arnd.
Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2022, Munich, Germany, 2nd April 2022. ed. / Clemens Dubslaff; Bas Luttik. 2022. p. 1-12 (EPTCS; Vol. 355).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

TY - GEN

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

AU - Hartmanns, Arnd

N1 - Conference code: 5

PY - 2022/3/21

Y1 - 2022/3/21

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

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

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

U2 - 10.4204/EPTCS.355.1

DO - 10.4204/EPTCS.355.1

M3 - Conference contribution

T3 - EPTCS

SP - 1

EP - 12

BT - Proceedings Fifth Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2022, Munich, Germany, 2nd April 2022

A2 - Dubslaff, Clemens

A2 - Luttik, Bas

T2 - 5th Workshop on Models for Formal Analysis of Real Systems 2022

Y2 - 2 April 2022 through 2 April 2022

ER -

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

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this