  Composition technologies improve reuse in the development of large-scale
complex systems. Safety critical systems require intensive validation and
verification activities. These activities should be compositional in order to
reduce the amount of residual verification activities that must be conducted on
the composite in addition to the ones conducted on each components. In order to
ensure the correctness of compositional verification and assess the minimality
of the residual verification, the contribution proposes to use formal
specification and verification at the composition operator level. A first
experiment was conducted in [15] using proof assistants to formalize the
generic composition technology ISC and prove that type checking was
compositional. This contribution extends our early work to handle full model
conformance and study the mandatory residual verification. It shows that ISC
operators are not fully compositional with respect to conformance and provides
the minimal preconditions on the operators mandatory to ensure compositional
conformance. The appropriate operators from ISC (especially bind) have been
implemented in the COQ4MDE framework that provides a full implementation of MOF
in the COQ proof assistant. Expected properties, respectively residual
verification, are expressed as post, respectfully pre, conditions for the
composition operators. The correctness of the compositional verification is
proven in COQ.
