27 October 2016 - 14h00
Modeling architectures and their properties in BIP
by Joseph Sifakis from VERIMAG
Abstract: Architectures are mechanisms for ensuring global properties characterizing the coordination between components. Using architectures largely accounts for our ability to master complexity and develop systems cost-effectively.
In BIP, architectures are generic behavior transformers represented as sets of connectors. They take as arguments typed components and give a composite component. We propose two different ways to describe architectures using respectively imperative and declarative languages. The imperative language, Dynamic BIP uses iterators on component variables and set-of-component variables to describe dynamic architectures. The declarative language is a second order Interaction Logic based on a symbolic representation of connectors.
In BIP, architecture properties are architecture styles or patterns that characterize families of architectures sharing common characteristics such as Token-ring and Philter styles. Configuration Logic is a power-set extension of Interaction Logic used to specify architecture styles.
We provide theoretical foundations of the above formalisms developed at EPFL and Verimag. We also provide examples illustrating their effective application.
We conclude with a discussion on ongoing and future work directions aiming at the implementation and integration of these results in correct-by-construction system design flows.