  This paper explores verification of constituent systems within the context of
the Symphony tool platform for Systems of Systems (SoS). Our SoS modelling
language, CML, supports various contractual specification elements, such as
state invariants and operation preconditions, which can be used to specify
contractual obligations on the constituent systems of a SoS. To support
verification of these obligations we have developed a proof obligation
generator and theorem prover plugin for Symphony. The latter uses the
Isabelle/HOL theorem prover to automatically discharge the proof obligations
arising from a CML model. Our hope is that the resulting proofs can then be
used to formally verify the conformance of each constituent system, which is
turn would result in a dependable SoS.
