Static analysis of real-time component-based systems configurations

Nowadays, more and more often, complex systems are built by assembling together different system components. This technology also affects the construction of heterogeneous and/or hybrid systems where components can represent hardware sensors, software controllers, etc. Moreover the resulting system is normally distributed. These systems have often real-time constraints/requirements and each component is characterized by its own speed determined by its local clock. In this paper we present a framework to specify and statically analyze the architecture of a system as a network of (parallel) components, each one with its own local clock. Configuring the system means to formally define how to get the global clock out of the local clocks. This clock configuration step is “optimal” that is, it is the best way to relate the local clocks so that the maximum number of synchronizations in the system can happen. Besides the usual behavioral and timing analysis, it is, for example, possible to verify if, and how changing the local speed of a component can affect the global performance of the system. Components behaviors are specified by means of a simple process algebra. Local clocks are modeled as higher order terms in a given signature, and unification is used to define the common clock. Then an operational semantics defines which transitions a process can perform and which transitions let time to elapse. A set of case studies illustrate the approach.