CSP||B is an integrated formal method approach which supports compositional verification.  Recently, we've been experimenting with using it alongside executable UML to expose weaknesses in concurrent state machines.

The work is very much in its preliminary phase and is part of a continuing 
industrial collaboration. In the talk I'll aim to show how we've tailored the style of CSP||B specficiations so that they can be applied to reason about UML state machines.