Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Reports, Documentation, and Standards
  4. Configuration Logics - Modelling Architecture Styles
 
report

Configuration Logics - Modelling Architecture Styles

Mavridou, Anastasia  
•
Baranov, Eduard  
•
Bliudze, Simon  
Show more
2015

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

MBBS15-ModellingArchs-TR.pdf

Access type

openaccess

Size

644.74 KB

Format

Adobe PDF

Checksum (MD5)

8b2a527b8dd4b6927b7153271f71fd24

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés