This example illustrates a formal verification of using a Message Sequence Chart (MSC) as a property to verify the behaviour implemented in a BPEL process.

This example expands on Iteration 1 by adding a 2nd scenario to the MSC specification.
Now the behaviour specifies that either GetVehicleRecords or GetVehicleInsuranceRecords may occur first.

1  In LTSA WS-Engineer switch the the Design tab 
2. Drag-and-drop both the pito.bpel and pito-msc.xml on to the tab page.
3. Switch the property to use as "Specification".
4. Click Verify and note that no violation occurs.

Resolution:

- The violation is resolved by wrapping both getvehiclerecords and getvehicleinsurancerecords invocation actions with a FLOW bpel construct. 
