Component-Based Software Engineering considers off-the-shelf software component reuse as its cornerstone. In previous work, we proposed Dedal, a three level Architecture Description Language. It supports a novel modeling approach that aims at describing the specification, the implemented configuration and the running assembly of the software. This eases reuse by guiding the search for existing components. In this paper, we propose a formal approach that states the rules for component reuse and interoperability among Dedal models. The use of B, a specifi- cation language providing model-checking capabilities, enables the automatic verification of Dedal architecture descriptions. The approach is illustrated using the example of a home automation software.