A general framework for architecture composability
Paul C. Attie, Eduard Baranov, Simon Bliudze, Mohamad Jaber, Joseph Sifakis · Formal Aspects of Computing · 2015
Abstract 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 Φ . Architecture composability is a basic and common problem faced by system designers. 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 A 1 and A 2 enforce respectively safety properties Φ 1 and Φ 2 , the architecture A 1 ⊕ A 2 enforces the property Φ 1 ∧ Φ 2 , that is both properties are preserved by architecture composition. We also establish preservation of liveness properties by architecture composition. The presented results are illustrated by a running example and a case study.