A general framework for architecture composability |
| |
Authors: | Paul Attie Eduard Baranov Simon Bliudze Mohamad Jaber Joseph Sifakis |
| |
Affiliation: | 1.American University of Beirut,Beirut,Lebanon;2.école Polytechnique Fédérale de Lausanne,Lausanne,Switzerland |
| |
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 ({mathcal{B}}), builds a composite component ({A(mathcal{B})}) meeting a characteristic property ({Phi}). 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 ({oplus}). The main result is that if two architectures A 1 and A 2 enforce respectively safety properties ({Phi_{1}}) and ({Phi_{2}}), the architecture ({A_{1} oplus A_{2}}) enforces the property ({Phi_{1} land Phi_{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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|