The design view of WS-Engineer provides verification of WS-BPEL orchestration process against that of design specifications in the form of UML style sequence charts. We model the interaction sequences built to support multiple-partner conversations across enterprise domains and with a view of wider goals. We limit the scope of choreography analysis to that of interactions between compositions.
The design view can be accessed by selecting the 
tab on the WS-Engineer view tab list.
You can skip to a particular topic of design analysis by selecting a button on the image below.
The essence of this verification is to prove that a property exists in the composition modelling of combined implementation and design models. Although the task of comparing models is easier in simple processes, more complex processes require an in-depth and time-consuming comparison. Model checking can then be performed to formally test that a WS-BPEL implementation provides the necessary activities to meet the MSC specification, through a model trace. Additionally, the aim is to provide as much a mechanical verification as possible, so that observation is not required by human eye in larger more complex processes.
You can read more about this type of verification in Chapter 6 of "A Rigorous Approach to Engineering Web Service Compositions" by Howard Foster Imperial College London.
|