TY - GEN
T1 - Towards a UTP semantics for modelica
AU - Foster, Simon
AU - Thiele, Bernhard
AU - Cavalcanti, Ana
AU - Woodcock, Jim
N1 - © 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.
PY - 2017/1/1
Y1 - 2017/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85010653555&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-52228-9
DO - 10.1007/978-3-319-52228-9
M3 - Conference contribution
AN - SCOPUS:85010653555
SN - 9783319522272
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 44
EP - 64
BT - Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers
A2 - Bowen, Jonathan P.
A2 - Zhu, Huibiao
PB - Springer
T2 - 6th International Symposium on Unifying Theories of Programming, UTP 2016
Y2 - 4 June 2016 through 5 June 2016
ER -