A general framework for architecture composability

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

Research output: Contribution to journalArticle

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 (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
Volume28
Issue number2
DOIs
StatePublished - Apr 1 2016
Externally publishedYes

Fingerprint

Chemical analysis
Composite materials
Architecture
Framework
Liveness
Composition Operator
Idempotent
Preservation
Correctness
Safety
Paradigm
Composite
Operator

Keywords

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

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science

Cite this

Attie, P., Baranov, E., Bliudze, S., Jaber, M., & Sifakis, J. (2016). A general framework for architecture composability. Formal Aspects of Computing, 28(2), 207-231. https://doi.org/10.1007/s00165-015-0349-8

A general framework for architecture composability. / Attie, Paul; Baranov, Eduard; Bliudze, Simon; Jaber, Mohamad; Sifakis, Joseph.

In: Formal Aspects of Computing, Vol. 28, No. 2, 01.04.2016, p. 207-231.

Research output: Contribution to journalArticle

Attie, P, Baranov, E, Bliudze, S, Jaber, M & Sifakis, J 2016, 'A general framework for architecture composability', Formal Aspects of Computing, vol. 28, no. 2, pp. 207-231. https://doi.org/10.1007/s00165-015-0349-8
Attie P, Baranov E, Bliudze S, Jaber M, Sifakis J. A general framework for architecture composability. Formal Aspects of Computing. 2016 Apr 1;28(2):207-231. https://doi.org/10.1007/s00165-015-0349-8
Attie, Paul ; Baranov, Eduard ; Bliudze, Simon ; Jaber, Mohamad ; Sifakis, Joseph. / A general framework for architecture composability. In: Formal Aspects of Computing. 2016 ; Vol. 28, No. 2. pp. 207-231.
@article{065021e2b5f04c9fb8a0f2483c4d2108,
title = "A general framework for architecture composability",
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 (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.",
keywords = "Architecture composability, BIP, Component-based frameworks, Liveness, Safety",
author = "Paul Attie and Eduard Baranov and Simon Bliudze and Mohamad Jaber and Joseph Sifakis",
year = "2016",
month = "4",
day = "1",
doi = "10.1007/s00165-015-0349-8",
language = "English (US)",
volume = "28",
pages = "207--231",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
publisher = "Springer London",
number = "2",

}

TY - JOUR

T1 - A general framework for architecture composability

AU - Attie, Paul

AU - Baranov, Eduard

AU - Bliudze, Simon

AU - Jaber, Mohamad

AU - Sifakis, Joseph

PY - 2016/4/1

Y1 - 2016/4/1

N2 - 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.

AB - 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.

KW - Architecture composability

KW - BIP

KW - Component-based frameworks

KW - Liveness

KW - Safety

UR - http://www.scopus.com/inward/record.url?scp=84950244711&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84950244711&partnerID=8YFLogxK

U2 - 10.1007/s00165-015-0349-8

DO - 10.1007/s00165-015-0349-8

M3 - Article

AN - SCOPUS:84950244711

VL - 28

SP - 207

EP - 231

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

IS - 2

ER -