A compositional modelling and analysis framework for stochastic
In Formal Methods in System Design
, 43: 191-232, 2013.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/s10703-012-0167-z
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.