By the same authors

Hybrid Relations in Isabelle/UTP

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

Full text download(s)

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publication7th International Symposium on Unifying Theories of Programming (UTP)
DateAccepted/In press - 12 Jul 2019
DatePublished (current) - 23 Sep 2019
Pages130-153
Number of pages24
PublisherSpringer
Original languageEnglish
ISBN (Electronic)9783030310387
ISBN (Print)9783030310370

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11885

Abstract

We describe our UTP theory of hybrid relations, which extends the relational calculus with continuous variables and differential equations. This enables the use of UTP in modelling and verification of hybrid systems, supported by our mechanisation in Isabelle/UTP. The hybrid relational calculus is built upon the same foundation as the UTP’s theory of reactive processes, which is accomplished through a generalised trace algebra and a model of piecewise-continuous functions. From this foundation, we give semantics to hybrid programs, including ordinary differential equations and preemption, and show how the theory can be used to reason about sequential hybrid systems.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations