"A Computable and Compositional Behavioural Framework for Continuous and Hybrid Systems"

For the verification of safety-critical complex cyber-physical systems, we need a framework which is:
 - Computable: the analysis can be performed on a digital computer and give rigorous results conforming to the mathematical semantics.
 - Compositional: components of the system can be independently analysed to show that  they conform to their own specification.
 - Behavioural: the analysis can be carried out at the level of the input-output behaviour, allowing for simplified concrete models to be used.
In this talk, I will present the computable, compositional and behavioural framework for hybrid systems developed in [*]. I will also discuss ongoing work on formalising the theory and rigorous numerical verification algorithms in the proof assistant Coq.

[*] Davide Bresolin, Pieter Collins, Luca Geretti, Roberto Segala, Tiziano Villa, and Sanja Zšivanovic Gonzalez. A computable and compositional semantics for hybrid systems. Information and Computation, 300:105189, 2024.