By the same authors

Towards a UTP semantics for modelica

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Full text download(s)

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publicationUnifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers
DateAccepted/In press - 15 Apr 2016
DatePublished (current) - 1 Jan 2017
Pages44-64
Number of pages21
PublisherSpringer Verlag
EditorsJonathan P. Bowen, Huibiao Zhu
Original languageEnglish
ISBN (Print)9783319522272

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10134 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Abstract

We describe our work on a UTP semantics for the dynamic systems modelling language Modelica. This is a language for modelling a system’s continuous behaviour using a combination of differential algebraic equations and an event-handling system. We develop a novel UTP theory of hybrid relations, inspired by Hybrid CSP and Duration Calculus, that is purely relational and provides uniform handling of continuous and discrete variables. This theory is mechanised in our Isabelle implementation of the UTP, Isabelle/UTP, with which we verify some algebraic properties. Finally, we show how a subset of Modelica models can be given semantics using our theory. When combined with the wealth of existing UTP theories for discrete system modelling, our work enables a sound approach to heterogeneous semantics for Cyber-Physical systems by leveraging the theory linking facilities of the UTP.

Bibliographical note

© 2016, Springer International Publishing AG. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Discover related content

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

View graph of relations