Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Architectures depict design principles, paradigms that can be understood by all, allow thinking on a higher plane and avoiding low-level mistakes. They provide means for ensuring correctness by construction by enforcing global properties characterizing the coordination between components. An architecture can be considered as an operator A that, applied to a set of components B, builds a composite component A(B) meeting a characteristic property P. Architecture composability is a basic and common problem faced by system designers. Consider two architectures A1, A2, enforcing respectively properties P1, P2 on a set of components B. That is, A1(B) and A2(B) satisfy respectively the properties P1 and P2. Is it possible to find an architecture A1 + A_2 such that the composite component (A1 + A2)(B) meets both P1 and P2? In this paper, we propose a formal and general framework for architecture composability based on an associative, commutative and idempotent architecture composition operator `+'. The main result is that if two architectures A1 and A2 enforce respectively state properties P1 and P2, the architecture A1 + A2 enforces the property P1 & P2, that is both invariants are preserved by architecture composition. We also discuss preservation of liveness properties of architecture composition. The presented results are illustrated by a running example and a case study.
,