Proving Component Interoperability with B Refinement

We use the formal method B for specifying interfaces of software components. Each component interface is equipped with a suitable data model defining all types occurring in the signature of interface operations. Moreover, pre- and postconditions have to be given for all interface operations. The interoperability between two components is proved by using a refinement relation between an adaptation of the interface specifications.