HYPE: Hybrid modelling by composition of flows

Vashti Galpin, Luca Bortolussi, Jane Hillston

Research output: Contribution to journalArticlepeer-review

Abstract

Hybrid systems are manifest in both the natural and the engineered world, and their complex nature, mixing discrete control and continuous evolution, make it difficult to predict their behaviour. In recent years several process algebras for modelling hybrid systems have appeared in the literature, aimed at addressing this problem. These all assume that continuous variables in the system are modelled monolithically, often with differential equations embedded explicitly in the syntax of the process algebra expression. In HYPE an alternative approach is taken which offers finer-grained modelling with each flow or influence affecting a variable modelled separately. The overall behaviour then emerges as the composition of flows. In this paper we give a detailed account of the HYPE process algebra, its semantics, and its use for verification of systems. We establish both syntactic conditions (well-definedness) and operational restrictions (well-behavedness) to ensure reasonable behaviour in HYPE models. Furthermore we consider how the equivalence relation defined for HYPE relates to other relations previously proposed in the literature, demonstrating that our fine-grained approach leads to a more discriminating notion of equivalence. We present the HYPE model of a standard hybrid system example, both establishing that our approach can reproduce the previously obtained results and demonstrating how our compositional approach supports variations of the problem in a straightforward and flexible way.
Original languageEnglish
Pages (from-to)503-541
Number of pages39
JournalFormal Aspects of Computing
Volume25
Issue number4
DOIs
Publication statusPublished - Jul 2013

Keywords

  • Hybrid systems
  • Process algebra
  • Flows
  • Compositionality
  • Bisimulation

Fingerprint

Dive into the research topics of 'HYPE: Hybrid modelling by composition of flows'. Together they form a unique fingerprint.

Cite this