A Semantic Framework for Architecture Modelling

Architectures are common means for organising coordination between components in order to build complex systems and to make them manageable. They allow thinking on a higher plane and avoiding low-level mistakes. Architectures provide means for ensuring correctness-by-construction by enforcing global properties characterising the coordination between components. In this work, we consider the following questions of architecture modelling: 1) how to model architectures; 2) how to compose them if several properties enforced by different architectures are required; 3) how to specify architectures styles that generalise the notion of architectures and represent families of architectures satisfying the same property. An architecture can be considered as an operator that, applied to a set of components, builds a composite component meeting a characteristic property. The underlying concepts of components and their interaction originate from the BIP framework. This thesis is structured in two parts. In the first part, we study the expressiveness of glue operators in the BIP framework. We provide results for classical BIP glue and for several modifications obtained by relaxing the constraints imposed on priority models. We also study an alternative semantics of BIP glue based on the offer predicate. It meets fundamental properties required from component-based frameworks, namely compositionality, incrementality, flattening and modularity. We provide the comparison with the classical BIP semantics and the algorithm for the synthesis of connectors from the interaction logic used to describe coordination constraints. In the second part, we define architectures and propose an architecture composition operator. We study their properties and prove that the composition operator preserves safety properties of its operands. The alternative glue semantics presented in the first part of the thesis allows to extend architectures with priorities. For the specification of architecture styles, we propose configuration logics. We provide a sound and complete axiomatisation of the propositional configuration logic as well as decision procedures for checking that an architecture satisfies a given logical specification. To allow genericity of specifications, we study higher-order extensions of the propositional configuration logic. We illustrate with examples the specification of various architecture styles. We provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for configuration logics. Additionally, we study the relation between the architecture composition operator and the composition of configuration logic formulas.

Configuration logics: Modeling architecture styles

Eduard Baranov, Simon Bliudze, Anastasia Mavridou, Joseph Sifakis

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of architectures as generic coordination schemes involving a configuration of interactions between typed components; and 2) configuration logics for the specification of architecture styles as sets of interaction configurations. The presented results build on previous work on architecture modeling in BIP. We show how propositional interaction logic can be extended into a corresponding configuration logic by adding new operators on sets of interaction configurations. In addition to the usual set-theoretic operators, configuration logic is equipped with a coalescing operator + to express combination of configuration sets. We provide a complete axiomatization of propositional configuration logic as well as decision procedures for checking that an architecture satisfies given logical specifications. To allow genericity of specifications, we study first-order and second-order extensions of the propositional configuration logic. First-order logic formulas involve quantification over component variables. Second-order logic formulas involve additional quantification over sets of components. We provide several examples illustrating the application of the results to the characterization of various architecture styles. We also provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for the propositional flavor of the logic.

Elsevier Science Inc2017

Configuration Logics - Modelling Architecture Styles

Eduard Baranov, Simon Bliudze, Anastasia Mavridou, Joseph Sifakis

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1)~interaction logics for the specification of architectures as generic coordination schemes involving a configuration of interactions between typed components; and 2)~configuration logics for the specification of architecture styles as sets of interaction configurations. Configuration logics can be considered as a power-set extension of interaction logics. The relation between the two logics is similar to the relation between programs and their specifications. As program specifications can be expressed, \eg in temporal logics, architecture styles can be specified in configuration logics. The presented results build on previous work on architecture modelling in BIP. We show how propositional interaction logic can be extended into a corresponding configuration logic by adding new operators on sets of interaction configurations. In addition to the usual set-theoretic operators, configuration logic is equipped with a coalescing operator + to express combination of configuration sets. This operator proves to be particularly useful for the specification of architecture styles including a given class of configurations. We provide a complete axiomatization of propositional configuration logic as well as decision procedures for checking that an architecture satisfies given logical specifications. To allow genericity of specifications, we study first-order and second-order extensions of the propositional configuration logic. First-order logic formulas involve quantification over component variables. Second-order logic formulas involve additional quantification over sets of components. We provide several examples illustrating the application of the results to the characterisation of various architecture styles. We also provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for the propositional flavour of the logic. We conclude with a discussion of the related work and of future directions dealing with the application of the results through the development of specific methods and tools.

2015

Modelling Architecture Styles

Anastasia Mavridou

Software systems tend to increase over time in size and complexity. Their development usually spans a long period of time and often results in systems that are hard to understand, debug and maintain. Architectures are common means for organising coordination between components in order to build complex systems and make them manageable. They allow thinking on a higher plane and avoiding low-level mistakes. Grouping architectures that share common characteristics into architecture styles assists component re-use and thus, the cost-effective development of systems. Additionally, architecture styles provide means for ensuring correctness-by-construction by enforcing global properties. The main goal of this thesis is to propose and study formalisms for modelling architectures and architecture styles. For the specification of architectures, we study interaction logics, which are Boolean algebras on a set of component actions. We study a modelling methodology based on first-order interaction logic for writing architecture constraints. To validate the applicability of the approach, we developed the JavaBIP framework that integrates architectures into mainstream software development. JavaBIP receives as input architecture specifications, which it then uses to coordinate software components without requiring access to their source code. JavaBIP implements the principles of the BIP component framework. For the specification of architecture styles, we propose configuration logics, which are powerset extensions of interaction logic. Propositional configuration logic formulas are generated from formulas of interaction logic by using the operators union, intersection and complementation, as well as a coalescing operator. We provide a complete axiomatisation of the propositional configuration logic and a decision procedure for checking that an architecture satisfies given logical specifications. To allow genericity of specifications, we study higher-order extensions of the propositional configuration logic. We provide several examples illustrating the application of configuration logics to the characterisation of architecture styles. For the specification of architecture styles, we also propose architecture diagrams, which is a graphical language rooted in rigorous semantics. We provide methods to assist software developers to specify consistent architecture diagrams, generate the conforming architectures of a style and check whether an architecture model meets given style requirements. We present a full encoding of architecture diagrams into configuration logics. Finally, we report on applications of architecture diagrams to modelling architecture styles identified in realistic case studies of on-board satellite software.

EPFL2016

Modelling Architecture Styles

Anastasia Mavridou

EPFL2016

Configuration Logics - Modelling Architecture Styles

Eduard Baranov, Simon Bliudze, Anastasia Mavridou, Joseph Sifakis

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1)~interaction logics for the specification of architectures as generic coordination schemes involving a configuration of interactions between typed components; and 2)~configuration logics for the specification of architecture styles as sets of interaction configurations. Configuration logics can be considered as a power-set extension of interaction logics. The relation between the two logics is similar to the relation between programs and their specifications. As program specifications can be expressed, \eg in temporal logics, architecture styles can be specified in configuration logics. The presented results build on previous work on architecture modelling in BIP. We show how propositional interaction logic can be extended into a corresponding configuration logic by adding new operators on sets of interaction configurations. In addition to the usual set-theoretic operators, configuration logic is equipped with a coalescing operator + to express combination of configuration sets. This operator proves to be particularly useful for the specification of architecture styles including a given class of configurations. We provide a complete axiomatization of propositional configuration logic as well as decision procedures for checking that an architecture satisfies given logical specifications. To allow genericity of specifications, we study first-order and second-order extensions of the propositional configuration logic. First-order logic formulas involve quantification over component variables. Second-order logic formulas involve additional quantification over sets of components. We provide several examples illustrating the application of the results to the characterisation of various architecture styles. We also provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for the propositional flavour of the logic. We conclude with a discussion of the related work and of future directions dealing with the application of the results through the development of specific methods and tools.

2015