Unsafe Message Exchange

Detected by Model Checking of BPEL

LTSA-WS: A Tool for Model-Based Verification
of Web Service Compositions and Choreography
Howard Foster, Sebastian Uchitel,
Jeff Magee, Jeff Kramer
Department of Computing, Imperial College London, UK, 2003.
doi=10.1.1.5.3846
Deadlock-free and Live, but
violates constraint on seller/buyer agreement.

©2012 Charles Petrie - permission to reproduce widely with attribution.