Towards a Logical Basis for the Specification of Reconfigurable Component-Based Systems
Due to the complexity and size of current software systems, the notion of structural architecture of systems, and its relationship to systems analysis and design, has come to play an important role in today's software development processes.<P>
Special specification languages, called architecture description languages (ADLs), were proposed to describe and analyse properties of (sometimes evolving) architectures. Many of these are able to deal with what is called dynamic reconfiguration, i.e., with the description of operations which may modify the system's structure at run time. While ADLs provide constructs for modelling the architecture of a system, they often do not support a language for reasoning about possible system evolution. In other words, ADLs support the definition of components, interconnections and transformation rules or operations for making architectures evolve, but any kind of reasoning about behaviours is often performed in some "meta-language", sometimes informally. Moreover, architectural elements in ADLs are usually described operationally, as opposed to declaratively.<P>
We wish, then, to be able to specify and reason about the consequences of using certain reconfiguration operations in a declarative manner, adding abstraction to what, to our understanding, can be operationally specified by ADLs.<P>
We adapt a logic proposed by Manna and Pnueli for the specification of reactive systems for this purpose. We present the logic and some results that make it suitable for the specification of dynamically reconfigurable systems. A (rather) prototypic language based on this logic is defined, where systems specifications are hierarchically organised around the following notions:
<P>
- the notion of components, which are represented by classes that define templates for these components;
<P>
- the notion of connector type, which we call associations, which are then used to define the potential ways in which components may be organised in a system;<P>
- the notion of subsystem, the new notion that defines the unit of modularity from which reconfigurable systems are built, and which conveys the information about what components, what associations and what reconfiguration operations are used to define the module.
