A compositional modelling and analysis framework for stochastic hybrid systems

Ernst Moritz Hahn, Arnd Hartmanns*, Holger Hermanns, Joost Pieter Katoen

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

99 Citations (Scopus)


The theory of hybrid systems is well-established as a model for real-world systems consisting of continuous behaviour and discrete control. In practice, the behaviour of such systems is also subject to uncertainties, such as measurement errors, or is controlled by randomised algorithms. These aspects can be modelled and analysed using stochastic hybrid systems. In this paper, we present HModest, an extension to the Modest modelling language - which is originally designed for stochastic timed systems without complex continuous aspects - that adds differential equations and inclusions as an expressive way to describe the continuous system evolution. Modest is a high-level language inspired by classical process algebras, thus compositional modelling is an integral feature. We define the syntax and semantics of HModest and show that it is a conservative extension of Modest that retains the compositional modelling approach. To allow the analysis of HModest models, we report on the implementation of a connection to recently developed tools for the safety verification of stochastic hybrid systems, and illustrate the language and the tool support with a set of small, but instructive case studies.

Original languageEnglish
Pages (from-to)191-232
Number of pages42
JournalFormal methods in system design
Issue number2
Publication statusPublished - Oct 2013
Externally publishedYes


  • Abstraction
  • Analysis
  • Modelling
  • Process calculus
  • Stochastic hybrid automata


Dive into the research topics of 'A compositional modelling and analysis framework for stochastic hybrid systems'. Together they form a unique fingerprint.

Cite this