Modern cyber-physical systems (CPS) present unique challenges as they are distributed
real-time systems used in many critical application domains, such as automotive or
railway systems. However, modeling and verifying the distributed and timed aspects
of the system are challenging tasks. We need a precise description of the possible
orderings of the components' execution, and a formal representation to be able to
run formal verification. In this paper, we investigate the possible extension of a
modeling and verification framework to support the flexible, configurable description
of the coordination of distributed critical systems. We present an extension of the
timed automata formalism, the coordination automata formalism, and show the applicability
of the extension on a motivating example.
