A General Framework for Architecture Composability

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 A1 and A2 enforce respectively safety properties Φ1 and Φ2, the architecture A1 ⊕ A2 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.


Editor(s):
Giannakopoulou, Dimitra
Salaün, Gwen
Published in:
Proceedings of the 12th International Conference on Software Engineering and Formal Methods, 8702, 128-143
Presented at:
12th International Conference on Software Engineering and Formal Methods, Grenoble, France, September 3-5, 2014
Year:
2014
Publisher:
Springer International Publishing
ISBN:
978-3-319-10430-0
Keywords:
Laboratories:




 Record created 2014-08-15, last modified 2018-03-17

Publisher's version:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)