Home - Modest Toolset
The Modest Toolset Contact us Documentation Examples Publications Download

Quantitative Modelling and Verification

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 [HHHK13] and supporting the JANI specification, it provides a variety of input languages and analysis backends.


Modelling formalisms 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:


The Modest Toolset currently supports the following input languages:

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:


The Modest Toolset can be downloaded for evaluation purposes.
We provide binaries for Windows, Linux and Mac OS. (System requirements)