Towards Configurable Coordination for Distributed Reactive Systems

Abstract

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.