A Formal Approach to Component Adaptation with a Tool Support

In a component-based software development, the only way to describe components is through interfaces since they are considered as black boxes. Indeed, their interfaces (required and provided) allow to express their visible behaviors. The connection between interfaces must be ensured in a suitable manner. The connection of two incompatible interfaces requires the use of a software adaptor. In this work, we define notions of compatibility between a required and a provided interfaces by focusing on protocol level. Then we specify adaptor in case of incompatibles intefaces. Finally, we check that compatibility by using the B formal method, based on the concept of refinement, and having powerful tool support, the B prover.