Verification of Compositional Frameworks in Coq

In this paper we aim to verify in Coq basic properties of compositional behavioural frameworks for dynamic systems. We analyse systems by their external behaviour rather than a state space model, and use the parallel composition operator to build complex systems from simpler subsystems. It is important that the composition is well-defined and avoids undesirable behaviour such as deadlocks. To ensure the our framework is correct, we formulate and prove the results in the proof assistant Coq. We consider discrete-time deterministic systems and timed-event systems, with a view to eventually proving results on a framework for hybrid systems.