Eduard Baranov, Simon Bliudze, Joseph Sifakis
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.
2014
