Isabelle/UTP

A verification toolbox for Isabelle/HOL based on Unifying Theories of Programming

View project on GitHub

Modelica

Modelica is a language for modelling dynamical systems using different equations. Products based on it include Dymola, Maple, Wolfram SystemModeler, and OpenModelica. We are currently working towards giving a mechanised formal semantics to its block-based control law diagram language in Isabelle/UTP making extensive use of the HOL’s Multivariate Analysis package and our own hybrid relational calculus. The latter extends the UTP relational calculus with continuous variables and ordinary differential equations (ODEs).

Modelica Blocks


Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure