Configuration Logics: Modelling Architecture Styles

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; 2) configuration logics for the specification of architecture styles as sets of interaction configurations. 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. We provide a complete axiomatisation of the propositional configuration logic, as well as a decision procedure 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. We provide examples illustrating the application of the results to the characterization of architecture styles. Finally, we provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for the propositional logic.

Braga, Christiano
Ölveczky, Peter Csaba
Published in:
Proceedings of the 12th International Conference on Formal Aspects of Component Software, 256--274
Presented at:
12th International Conference on Formal Aspects of Component Software, Niterói, Rio de Janeiro, Brazil, October 14-16, 2015
Cham, Springer Int Publishing Ag
978-3-319-28934-2; 978-3-319-28933-5

 Record created 2015-10-21, last modified 2018-03-17

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)