The Modest Toolset: An integrated environment for quantitative modelling and verification

Abstract

Probabilities, real-time behaviour and continuous dynamics are the key ingredients of quantitative models enabling formal studies of non-functional properties such as dependability and performance. The Toolset is based on networks of stochastic hybrid automata (SHA) as an overarching semantic foundation. Many existing automata-based formalisms are special cases of SHA. The toolset aims to facilitate reuse of modelling expertise via Modest, a high-level compositional modelling language; to allow reuse of existing models by providing import and export facilities for existing languages; and to permit reuse of existing tools by integrating them in a unified modelling and analysis environment. © 2014 Springer-Verlag.