mctau: Bridging the Gap between Modest and UPPAAL. Modest is a high-level compositional modelling language for stochastic timed systems with a formal semantics in terms of stochastic timed automata, an overarching formalism of which several well-studied models are special cases. The emphasis of Modest is to make use of existing analysis techniques and tools in a single-formalism, multiple-solution approach. In this paper, we focus on networks of timed automata as supported by Uppaal. We report on extensions made to Modest and Uppaal that allow the transformation of a rich subset of Modest models to Uppaal timed automata and enable connections to further tools and formalisms. We present our Modest-to-Uppaal tool chain mctau, which allows both a fully automated analysis as well as model transformation, and we compare its performance with the existing mcpta tool.

References in zbMATH (referenced in 2 articles )

Showing results 1 to 2 of 2.
Sorted by year (citations)

  1. Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter: A compositional modelling and analysis framework for stochastic hybrid systems (2013)
  2. Bogdoll, Jonathan; David, Alexandre; Hartmanns, Arnd; Hermanns, Holger: mctau: bridging the gap between Modest and UPPAAL (2012) ioport