Verifying the correct composition of distributed components: Formalisation and Tool

TL;DR

This paper formalizes the concept of well-formed component composition to ensure safe deployment and execution, providing a comprehensive foundation for component-based system development and verification.

Contribution

It introduces a formalization of component architecture concepts, integrating functional and non-functional aspects, and provides an Eclipse-based tool for development and specification.

Findings

Formal definitions guarantee correct component architectures

Interceptor chains enable safe interaction between aspects

The formalization underpins a development environment for component systems

Abstract

This article provides formal definitions characterizing well-formed composition of components in order to guarantee their safe deployment and execution. Our work focuses on the structural aspects of component composition; it puts together most of the concepts common to many component models, but never formalized as a whole. Our formalization characterizes correct component architectures made of functional and non-functional aspects, both structured as component assemblies. Interceptor chains can be used for a safe and controlled interaction between the two aspects. Our well-formed components guarantee a set of properties ensuring that the deployed component system has a correct architecture and can run safely. Finally, those definitions constitute the formal basis for our Eclipse-based environment for the development and specification of component-based applications.