modestchecker.net - Home - Modest Toolset

home > domains > modestchecker.net

Example domain paragraphs

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.

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:

Links to modestchecker.net (4)

• jani-spec.org The JANI Specification
• marnixsuilen.nl Marnix Suilen' webpage
• formal-verification-research.github.io USU Formal Verification Research
• momba.dev Welcome to Momba’s documentation! — Momba