A general framework for architecture composability

Paul Attie, Eduard Baranov, Simon Bliudze, Mohamad Jaber, Joseph Sifakis

Research output: Contribution to journalArticlepeer-review

25 Scopus citations


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 (Formula presented.) , builds a composite component (Formula presented.) meeting a characteristic property (Formula presented.). 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 (Formula presented.). The main result is that if two architectures A1 and A2 enforce respectively safety properties (Formula presented.) and (Formula presented.) , the architecture (Formula presented.) enforces the property (Formula presented.) , 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.

Original languageEnglish (US)
Pages (from-to)207-231
Number of pages25
JournalFormal Aspects of Computing
Issue number2
StatePublished - Apr 1 2016
Externally publishedYes


  • Architecture composability
  • BIP
  • Component-based frameworks
  • Liveness
  • Safety

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software


Dive into the research topics of 'A general framework for architecture composability'. Together they form a unique fingerprint.

Cite this