Trustworthy Assembly of Components using B Refinement

In component-based software development approaches, components are considered as black boxes, communicating through required and provided interfaces which describe their visible behaviors. In the best cases, the provided interfaces are checked to be compatible with the corresponding required interfaces, but in general, adapters have to be introduced to connect them. We propose to exploit existing notations and languages with their associated tools to specify working systems out of components: UML composite structure diagrams to express the architecture in terms of components and their interfaces, class diagrams, sequence diagrams and protocol state machines to describe the behavior of each component. Component interfaces will then be expressed in B in order to verify the interoperability. The use of B assembling and refinement mechanisms eases the verification of the interoperability between interfaces and the correctness of the component assembly.