A compositional modelling and analysis framework for stochastic hybrid systems

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

Research output: Contribution to journalArticle

65 Citations (Scopus)

Abstract

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
Volume43
Issue number2
DOIs
Publication statusPublished - 2013
Externally publishedYes

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

  • Cite this