The Modest Toolset supports the modelling and analysis of hybrid, real-time, distributed and stochastic systems. A modular framework centered around the stochastic hybrid automata formalism [HHHK12], it provides a variety of input languages and analysis backends.
At the core of the Modest Toolset is the model of networks of stochastic hybrid automata (SHA), which combine nondeterministic choices, continuous system dynamics, stochastic decisions and timing, and real-time behaviour, including nondeterministic delays. A wide range of well-known and extensively studied formalisms in modelling and verification can be seen as special cases of SHA:
- STA (stochastic timed automata), the original semantic foundation of Modest [BDHK06], are SHA without complex continuous behaviour (i.e. without variables whose evolution over time is governed by differential equations or inclusions, except for clock variables).
- PTA (probabilistic timed automata) are obtained from STA by restricting stochastic decisions to choices based on finite-support probability distributions (such as the discrete uniform or the Bernoulli distribution).
- TA (timed automata) are non-probabilistic PTA. Delays and discrete choices can still be nondeterministic, but not stochastic. TA are widely used to model real-time systems and requirements.
- PA/MDP (probabilistic automata/Markov decision processes), on the other hand, can be seen as PTA without the notion of time, i.e. without clock variables or delays. PA theory focuses on compositionality and simulation relations between models, while MDP are usually considered with costs or rewards, but both are essentially the same model.
- LTS (labelled transition systems), alternatively Kripke structures or finite automata, are the most basic, fundamental model for verification. Allowing nondeterministic choices, they are supported by a wide range of model-checking tools of impressive scalability.
- DTMC (discrete-time Markov chains) are the basic discrete probabilistic model. As a model without nondeterminism, they are not only amenable to a wide range of numerical analysis approaches, but also ideally suited for simulation.
- CTMC, IMC and MA (continuous-time Markov chains, interactive Markov chains and Markov automata) form the family of stochastic models based on the notion of exponentially distributed delays, which can be represented in STA via a combination of sampling from the exponential distribution and subsequently waiting the sampled amount of time using a dedicated clock variable.
The Modest Toolset currently supports the following input languages:
- Modest: a high-level compositional modelling language for stochastic hybrid systems [HHHK12].
- Guarded commands: a low-level modelling language, compatible with the PRISM probabilistic model checker.
- UPPAAL TA: networks of timed automata modelled graphically in the UPPAAL tool environment.
Due to the toolset's modular nature, new input languages can easily be added by implementing a small set of interfaces and providing a semantics in terms of SHA.
The Modest Toolset comprises the following tools:
- mime is a cross-platform graphical user interface that provides an integrated environment for modelling and analysis, including an interface to all analysis tools.
- prohver [HHHK12] model-checks probabilistic safety properties of SHA.
- mcpta [HH09] uses PRISM to allow model checking of unbounded, time- and cost-bounded probabilistic, expected-time and expected-reward reachability properties of PTA.
- mctau [BDHH12] connects to UPPAAL for efficient model checking of TA and the non-probabilistic overapproximation of PTA.
- modes [BHH12] allows the approximative analysis of STA using statistical model checking and the generation of simulation traces through models. Its emphasis is on the sound treatment of nondeterministic choices in simulation.
- mosta helps visualise the SHA semantics of a model by generating a graphical representation of the automata.