Modeling architectures and their properties

Architectures are common means for organizing coordination between components in order to build complex systems and to make them manageable. Despite the progress of the state of the art over the past decades, there are still a lot of foundational issues that remain unsolved. In this talk we present a general framework for modeling architectures and their properties. The framework considers that systems are obtained as the composition of atomic components by using glue operators. These are composition operators on components. Their meaning can be specified by operational semantics rules giving the global behavior of a composite component as a function of the behaviors of its constituents. They implicitly define connectors between components each connector involving multiparty interaction and an associated atomic computation modifying the state of the composed components. We present results characterizing the expressiveness of glue operators and show that universal expressiveness can be achieved by using a limited and well-defined set of types of connectors. We also propose a powerful notation for connectors encompassing both static and dynamic coordination. Architectures can be considered as generic operators parameterized by types of coordinator components and glue operators. Applied to a set of components they enforce a characteristic property on the resulting global behavior. Coordinators are needed only when the types of glue operators are not expressive enough for achieving the desired coordination. The proposed formalization of architectures can be used for building component-based systems that are correct by construction. We present composability results, which guarantee preservation of the characteristic behavioral properties of a set of architectures when they are jointly applied to the same operands. We present logics for the description of architectural properties. Formulas of these logics characterize architectural styles as the description of component types from which a system is built, and their interconnection. The presented logics include a propositional logic and two higher-order extensions of this logic. We provide an axiomatization of the propositional logic as well as results on the expressiveness of the higher-order logics and their effective application for the description of architectural styles.