Hybrid systems are dynamic systems combining discrete and continuous behaviour. It is important to have powerful modelling frameworks which support modular design via composition of subsystems, and automated software tools for simulation and verification. Unfortunately, it is a nontrivial task to provide a behavioural semantics for a modelling framework which is computable in the sense that true properties are provable by numerical algorithms and which respects also the parallel composition operator. In this talk I will give compositional and computable semantics for a restricted subset of models specified using the Compositional Interchange Format (CIF) for modelling hybrid systems. The CIF already has a well-defined standard operational semantics, we introduce an upper-semicomputable semantics for proving safety properties and a lower-semicomputable semantics for proving liveness properties. Finally, I will give example of an automatic translation of a simple CIF model to the API of the reachability analysis tool Ariadne.

Joint work with Ramon Schiffelers and Bert van Beek (TU/e), Davide Bresolin and Tiziano Villa (Verona) and Ivan Zapreev (CWI)