Modest Models and Tools for Real Stochastic Timed Systems

Carlos E. Budde; Pedro R. D’Argenio; Juan A. Fraire; Arnd Hartmanns; Zhen Zhang

doi:10.1007/978-3-031-75775-4_6

Modest Models and Tools for Real Stochastic Timed Systems

Carlos E. Budde, Pedro R. D’Argenio, Juan A. Fraire, Arnd Hartmanns^*, Zhen Zhang

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

1 Citation (Scopus)

13 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. This paper gives an introduction to quantitative verification using the Modest modelling language and the Modest Toolset. It highlights 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 needs Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. For each, we explain the particular conceptual and technical challenges in modelling and verification, and point out open problems for future work.

Original language	English
Title of host publication	Principles of verification: Cycling the probabilistic landscape
Subtitle of host publication	Essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday, Part II
Editors	Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk
Place of Publication	Cham, Switzerland
Publisher	Springer
Pages	115-142
Number of pages	28
ISBN (Electronic)	978-3-031-75775-4
ISBN (Print)	978-3-031-75774-7
DOIs	https://doi.org/10.1007/978-3-031-75775-4_6
Publication status	Published - 2025

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	15261
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

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.
2025 OA procedure

Access to Document

10.1007/978-3-031-75775-4_6

ArticleFinal published version, 898 KBLicence: Taverne

Cite this

Budde, C. E., D’Argenio, P. R., Fraire, J. A., Hartmanns, A., & Zhang, Z. (2025). Modest Models and Tools for Real Stochastic Timed Systems. In N. Jansen, S. Junges, B. L. Kaminski, C. Matheja, T. Noll, T. Quatmann, M. Stoelinga, & M. Volk (Eds.), Principles of verification: Cycling the probabilistic landscape: Essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday, Part II (pp. 115-142). (Lecture Notes in Computer Science; Vol. 15261). Springer. https://doi.org/10.1007/978-3-031-75775-4_6

Budde, Carlos E. ; D’Argenio, Pedro R. ; Fraire, Juan A. et al. / Modest Models and Tools for Real Stochastic Timed Systems. Principles of verification: Cycling the probabilistic landscape: Essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday, Part II. editor / Nils Jansen ; Sebastian Junges ; Benjamin Lucien Kaminski ; Christoph Matheja ; Thomas Noll ; Tim Quatmann ; Mariëlle Stoelinga ; Matthias Volk. Cham, Switzerland : Springer, 2025. pp. 115-142 (Lecture Notes in Computer Science).

@inbook{db0ee98f6713403c99efaa1d0c2e0b30,

title = "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. This paper gives an introduction to quantitative verification using the Modest modelling language and the Modest Toolset. It highlights 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 needs Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. For each, we explain the particular conceptual and technical challenges in modelling and verification, and point out open problems for future work.",

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., 2025 OA procedure",

author = "Budde, \{Carlos E.\} and D{\textquoteright}Argenio, \{Pedro R.\} and Fraire, \{Juan A.\} and Arnd Hartmanns and Zhen Zhang",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.",

year = "2025",

doi = "10.1007/978-3-031-75775-4\_6",

language = "English",

isbn = "978-3-031-75774-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "115--142",

editor = "Nils Jansen and Sebastian Junges and Kaminski, \{Benjamin Lucien\} and Christoph Matheja and Thomas Noll and Tim Quatmann and Mari{\"e}lle Stoelinga and Matthias Volk",

booktitle = "Principles of verification: Cycling the probabilistic landscape",

address = "Germany",

}

Budde, CE, D’Argenio, PR, Fraire, JA, Hartmanns, A & Zhang, Z 2025, Modest Models and Tools for Real Stochastic Timed Systems. in N Jansen, S Junges, BL Kaminski, C Matheja, T Noll, T Quatmann, M Stoelinga & M Volk (eds), Principles of verification: Cycling the probabilistic landscape: Essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday, Part II. Lecture Notes in Computer Science, vol. 15261, Springer, Cham, Switzerland, pp. 115-142. https://doi.org/10.1007/978-3-031-75775-4_6

Modest Models and Tools for Real Stochastic Timed Systems. / Budde, Carlos E.; D’Argenio, Pedro R.; Fraire, Juan A. et al.
Principles of verification: Cycling the probabilistic landscape: Essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday, Part II. ed. / Nils Jansen; Sebastian Junges; Benjamin Lucien Kaminski; Christoph Matheja; Thomas Noll; Tim Quatmann; Mariëlle Stoelinga; Matthias Volk. Cham, Switzerland: Springer, 2025. p. 115-142 (Lecture Notes in Computer Science; Vol. 15261).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Modest Models and Tools for Real Stochastic Timed Systems

AU - Budde, Carlos E.

AU - D’Argenio, Pedro R.

AU - Fraire, Juan A.

AU - Hartmanns, Arnd

AU - Zhang, Zhen

N1 - Publisher Copyright: © The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

PY - 2025

Y1 - 2025

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. This paper gives an introduction to quantitative verification using the Modest modelling language and the Modest Toolset. It highlights 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 needs Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. For each, we explain the particular conceptual and technical challenges in modelling and verification, and point out open problems for future work.

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. This paper gives an introduction to quantitative verification using the Modest modelling language and the Modest Toolset. It highlights 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 needs Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. For each, we explain the particular conceptual and technical challenges in modelling and verification, and point out open problems for future work.

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.

KW - 2025 OA procedure

UR - https://www.scopus.com/pages/publications/85213044853

U2 - 10.1007/978-3-031-75775-4_6

DO - 10.1007/978-3-031-75775-4_6

M3 - Chapter

AN - SCOPUS:85213044853

SN - 978-3-031-75774-7

T3 - Lecture Notes in Computer Science

SP - 115

EP - 142

BT - Principles of verification: Cycling the probabilistic landscape

A2 - Jansen, Nils

A2 - Junges, Sebastian

A2 - Kaminski, Benjamin Lucien

A2 - Matheja, Christoph

A2 - Noll, Thomas

A2 - Quatmann, Tim

A2 - Stoelinga, Mariëlle

A2 - Volk, Matthias

PB - Springer

CY - Cham, Switzerland

ER -

Budde CE, D’Argenio PR, Fraire JA, Hartmanns A, Zhang Z. Modest Models and Tools for Real Stochastic Timed Systems. In Jansen N, Junges S, Kaminski BL, Matheja C, Noll T, Quatmann T, Stoelinga M, Volk M, editors, Principles of verification: Cycling the probabilistic landscape: Essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday, Part II. Cham, Switzerland: Springer. 2025. p. 115-142. (Lecture Notes in Computer Science). Epub 2024 Nov 13. doi: 10.1007/978-3-031-75775-4_6

Modest Models and Tools for Real Stochastic Timed Systems

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Cite this