A Model of Layered Architectures

TL;DR

This paper provides a formal, denotational semantics for layered architecture styles in software engineering, enabling precise analysis and conformance checking of systems to this architectural pattern.

Contribution

It introduces a rigorous, abstract formal model of layered architectures, including relations between services and dependency notions, to improve clarity and verification.

Findings

Formal semantics for layered architectures established

Relations between syntactic and semantic dependencies analyzed

Conditions identified where dependencies coincide or imply each other

Abstract

Architectural styles and patterns play an important role in software engineering. One of the most known ones is the layered architecture style. However, this style is usually only stated informally, which may cause problems such as ambiguity, wrong conclusions, and difficulty when checking the conformance of a system to the style. We address these problems by providing a formal, denotational semantics of the layered architecture style. Mainly, we present a sufficiently abstract and rigorous description of layered architectures. Loosely speaking, a layered architecture consists of a hierarchy of layers, in which services communicate via ports. A layer is modeled as a relation between used and provided services, and layer composition is defined by means of relational composition. Furthermore, we provide a formal definition for the notions of syntactic and semantic dependency between the layers. We show that these dependencies are not comparable in general. Moreover, we identify sufficient conditions under which, in an intuitive sense which we make precise in our treatment, the semantic dependency implies, is implied by, or even coincides with the reflexive-transitive closure of the syntactic dependency. Our results provide a technology-independent characterization of the layered architecture style, which may be used by software architects to ensure that a system is indeed built according to that style.