Modest Toolset

Home

Home Downloads Publications Case Studies Documentation Contact Us More Tools

The Modest Toolset is a collection of programs that support the construction and analysis of models specified in the Modest language for real-time, distributed and stochastic systems.

The Language

Modest is a high-level, compositional formal modelling language for stochastic timed systems. It combines concepts such as nondeterminism, probabilistic branching, real time and continuous probability distributions in an orthogonal way such that precisely defined subsets of the language correspond to well-known models that are amenable to model-checking, for example Probabilistic Timed Automata (PTA) or Continuous-time Markov Chains (CTMCs).

The Tools

mime

mime is the integrated modelling environment for Modest that combines a Modest editor with syntax highlighting and error highlighting with direct access to the model analysis capabilities of mcpta and modes.

mime makes modelling more efficient by immediately reporting errors during model construction, and it makes the model analysis more convenient and accessible by integrating it in a single graphical tool. Of course, mime remembers all your open files as well as your analysis settings—there's no need to type dozens of constant values for your experiments every time you'd like to run your analysis.

mcpta

mcpta is a model-checking tool for the subset of Modest that corresponds to probabilistic timed automata (PTA). It translates Modest models of PTA into the guarded command language used by PRISM and other probabilistic model-checkers, using a digital clocks semantics for time.

mcpta can thus be used to specify models that combine discrete probabilistic choices, for example the transmission of a message failing with probability 0.1, with real-time behaviour, such as the time a transmission needs being anywhere between 5 and 20 µs. Properties that can be verified using mcpta include probabilistic and probabilistic time-bounded reachability properties, like "what is the maximum probability that communication succeeds within 2 seconds", as well as expected-time reachability properties—e.g. "what is the expected time until both parties have sent their message successfully".

modes

modes analyses Modest models using discrete-event simulation, including proper treatment of nondeterministic models—an area where many other simulation tools rely on hidden assumptions that may affect the results in unexpected ways.

modes places almost no restrictions on the use of Modest's language features, allowing fully recursive processes and full dynamic parallelism. However, this allows the specification of nondeterministic models—but discrete-event simulation always needs fully determined specifications. By default, modes will thus reject these kinds of models. It also provides several options to the user to change this behaviour, which include random resolution as implicitly used by most other simulators, but also a novel approach based on partial-order reduction techniques that tries to identify and ignore spurious nondeterminism on-the-fly.

Download

The Modest Toolset can be downloaded for evaluation purposes.
The command-line tools, mcpta and modes, have been tested on Windows and Linux; mime only runs on Windows.