We propose a method for component-based software and system development, where the interoperability between the different components is given special consideration. The method uses existing notations and languages with their associated tools: context diagrams for analyzing and structuring the problem, composite structure diagrams for describing the overall system in terms of components and interfaces, sequence diagrams to describe the behavior of each component, and the formal method B for specifying the interfaces of the different components and for proving their interoperability. The method proposes to integrate these different notations; at the end of the process, the interoperability is guaranted by the use of the B method with its underlying concept of refinement, and its powerful tool support, the B prover.
