Towards a UTP semantics for modelica

Simon Foster*, Bernhard Thiele, Ana Cavalcanti, Jim Woodcock

*Corresponding author for this work

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

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.

Original languageEnglish
Title of host publicationUnifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers
EditorsJonathan P. Bowen, Huibiao Zhu
PublisherSpringer
Pages44-64
Number of pages21
ISBN (Print)9783319522272
DOIs
Publication statusPublished - 1 Jan 2017
Event6th International Symposium on Unifying Theories of Programming, UTP 2016 - Reykjavik, Iceland
Duration: 4 Jun 20165 Jun 2016

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

Conference

Conference6th International Symposium on Unifying Theories of Programming, UTP 2016
Country/TerritoryIceland
CityReykjavik
Period4/06/165/06/16

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.

Cite this