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

TL;DR

This paper reviews the use of Modest models and tools for verifying stochastic timed systems in cyber-physical applications, highlighting recent case studies involving Markov models and decision processes.

Contribution

It provides an overview of Modest's capabilities for modeling and verifying complex stochastic timed systems, illustrated through recent practical case studies.

Findings

Power supply noise modeled as Markov chain

Satellite message routing with Markov decision processes

Bitcoin attack optimization using Markov automata

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.