Specifying and Composing Layered Architectures

We define the layered architectural style as an architectural pattern and a structuring method in terms of precise specifications of interface behavior and modular composition, based on a formal model. Interface predicates and interface assertions are used to specify the interface behavior of systems, which is a description of the services that they require and provide. We give both a syntactic and a semantic description of the design pattern of layered system architectures. Moreover, we prove that the composition of multiple layers also generates layers, subject to the condition that the services provided by lower layers are refinements of the required services of upper layers. We demonstrate the approach by examples. We seek two goals: (a) to give a precise semantic characterization of the concept of layered architectures, and (b) to provide a method for specifying and for structuring layered system architectures. We show how to decompose services as offered and used by layered architectures into encapsulated subservices called functional features. A related issue is the identification of feature interactions between these subservices. Feature interactions between functional features can be identified by studying their interface behavior. A number of small examples is given to illustrate the introduced notions and concept.