Modest Toolset
Subproject |
S2 |
Categories |
Model checker for hard & soft real-time systems, Model checker / solver for probabilistic systems |
Overview |
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: 1) modes analyses Modest models using discrete-event simulation, including proper treatment of nondeterministic models. It provides several options to the user to control the way nondeterminism is handled, 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. 2) mcpta is a model-checking tool for probabilistic timed automata. 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. 3) mime is the integrated modelling environment for Modest that combines a syntax- and error-highlighting editor with direct access to the model analysis capabilities of mcpta and modes. |
J. Bogdoll, L. M. Ferrer Fioriti, A. Hartmanns and H. Hermanns. Partial Order Methods for Statistical Model Checking and Simulation. In 13th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems and 31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems (FMOODS/FORTE), 2011. A. Hartmanns and H. Hermanns. A Modest Approach to Checking Probabilistic Timed Automata. In Sixth International Conference on Quantitative Evaluation of Systems (QEST 2009), 2009. |
|
Benchmarks |
|
Download |
|
Manual |
|
Status |
Stable |