Hierarchical Temporal Specifications of Dynamically Reconfigurable Component Based Systems

We study how temporal specifications of reconfigurable component based systems can be hierarchically organised. We do so by extending a previously introduced declarative prototypical language to admit the definition of hierarchical subsystems. Each subsystem has an internal architecture, composed of its internal interacting (simpler) subsystems, and basic components. The internal architecture of a subsystem can change at “run time” by means of reconfiguration operations. The notion of subsystem provides an extra coarse grained unit of modularisation, that complements that of components. Since component interaction is achieved by means of coordination, a component or subsystem can be represented by a logical theory isolated from the rest of the system. This, in combination with the possibility of hierarchically organising a specification, has a special impact in reasoning, since it allows us to further localise the proof efforts to the relevant subparts of a specification.