Instance Isolation Analysis for Service-Oriented Architectures

When a service engages in multiple conversations concurrently, incoming messages must be correlated with messages previously sent or received. Languages such as BPEL incorporate correlation as first-class citizen. However, current verification and testing techniques for service implementations largely ignore possible correlation anomalies as they typically focus on isolated conversations. This paper defines the notion of instance isolation and shows how to check this property. For doing so it introduces v*-nets, a Petri net extension with name creation and name passing.