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).
Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure