In this overview paper accompanying my invited presentation at the 5th Workshop on Models for Formal Analysis of Real Systems (MARS 2022), I outline two such modelling languages, Modest and JANI, and one such set of tools, the Modest Toolset (in sec:Modest).
I then briefly summarise how Modest and the Modest Toolset have been used
to study power supply noise in a two-by-two network-on-chip system by way of a discrete-time Markov chain (DTMC) model and probabilistic model checking with the mcsta tool (in sec:NoC);
to find routes through sparse constellations of nanosatellites using an abstract Markov decision process (MDP) [1]}, [2]} model analysed with a statistical model checking approach that employs scheduler sampling under distributed information as implemented in the modes tool (in sec:Space);
and to optimise an attack on the Bitcoin cryptocurrency system via a Markov automata (MA) [3]} model that permits mcsta to synthesise the strategy that minimises the expected time to success or maximises the probability of success within a certain time bound (in sec:Bitcoin).
