PV3 ⊧ Modest Toolseta collection of stochastic model checkers

Toolset for modelling and analysis of hybrid, real-time distributed and stochastic systems

Application domain/field

• Model checking
• Hybrid systems
• Real-time systems
• Distributed systems
• Stochastic systems

Type of tool

Combination of several tools include model checkers and translators.

Expected input

Format:

Modest toolset (own) format or JANI format.

Internals

The tool consists of the following tools:

• mcsta: disk-based explicit-state model checker for STA, PTA and MDP
• moconv: converts models between Modest's input language to the JANI format and back
• modes: statistical model checker for SHA, STA, PTA and MDP
• modysh: probabilistic model checker for MDP based on dynamic search and heuristic planning techniques
• mosta: generates a graphical representation of a SHA
• prohver: safety model checker for SHA

Comments

• STA: Stochastic Timed Automata
• PTA: Probabilistic Timed Automata
• MDP: Markov Decision Processes
• SHA: Stochastic Hybrid Automata