The modes view of WS-Engineer provides both verification of service modes architecture specifications and automated generation of Service Broker requirements for those modes.
A service mode architecture consists of a series of mode service collaborations. Typically this will be constructed in UML2 (with a Service Modes profile applied). UML2 Component Structure, Constraints, Activity, Sequence and State Machine Diagrams are translated to formal models and analysed for consistency and correctness.
You can read more about this type of verification in the following publication(s):
H.Foster, S.Uchitel, J.Kramer, J.Magee, Towards Self-Management in Service-oriented Computing with Modes , in Proceedings of the Workshop on Engineering Service-Oriented Applications (WESOA07), Vienna, Austria. Sept 2007.
H.Foster, A.Mukhija, S.Uchitel and D.Rosenblum, A Model-Driven Approach to Dynamic and Adaptive Service Brokering using Modes, in Proceedings of the 6th International Conference on Service Oriented Computing (ICSOC 2008), Sydney, Australia. December 2008.