Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
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 P. A theory of architectures must address several fundamental questions: 1. How does one model the architectures? In many existing approaches, architecture description is limited to drawing the structure of the system by connecting boxes with lines. A rigorous theory requires a formal definition of their operational semantics. 2. How does one specify the architectures? Characteristic properties of architectures must be clearly stated, understandable and verifiable by engineers. Specifications must be sufficiently versatile for the architectures to be applicable to a variety of components. 3. How does one combine architectures? Composition of architectures must preserve their respective characteristic properties. 4. How does one efficiently implement architectures? The cost of raising the abstraction level is the coordination overhead entailed by any centralised framework imposing the operational semantics. This can be reduced by applying transformation techniques to internalise and distribute the coordination constraints. We propose a formal and general framework for studying architectures. In particular, composability is based on an associative, commutative and idempotent architecture composition operator. The main result is that if two architectures A1 and A2 enforce respectively state invariants P1 and P2 , the composed architecture enforces the state invariant P1 & P2, that is both invariants are preserved by architecture composition. We also discuss preservation of liveness properties and internalisation of architectures.
Francesco Mondada, Robert Matthew Mills
André Patrão Neves De Frias Martins