Modern cyber-physical systems (CPS) are distributed reactive real-time systems used
in many critical application domains, such as automotive or railway systems, so ensuring
their correctness is essential. Formal verification can exhaustively explore the behavior
of the formal representation of CPS to ensure its reliability. Engineering modeling
tools provide separate modeling constructs for the different aspects of the systems,
e.g., behavior, architecture, and scheduling, but lack formal composition, making
system-level verification difficult. Formal modeling tools, e.g., Lingua Franca or
the Gamma Statechart Composition Framework, are efficient in describing component
behavior, and they provide formal composition semantics of the subsystems. However,
the provided composition patterns in these languages are not general, so incorporating
the precise coordination, scheduling, and interaction aspects requires the modification
of the component models by encoding the coordination into the components. In this
paper, we present a configurable formal description approach for the coordination
of distributed critical systems. We extend the well-known timed automata formalism
to coordinate the execution of the components by directly reusing the formal models
of the components, making the coordination of the system components a first-class
citizen.
