A Model of Scope for Verification of Implementation of Choreography with Exception Handler Using UPPAAL

Web service choreography description language (WS-CDL) choreographies describe peer-to-peer collaboration between participating web services and their obligations. Several formal models have been, proposed for verification of correct implementation of these collaboration and obligations in Web service business process execution language (WS-BPEL). However, these models did not address temporal constraints of WS-CDL interaction, and transformation of exception handler, finalizer block and scope with fault and compensation handler to extended-timed-automata (ETA). Transformation rules for these constructs are needed to address all possible scenarios of verification. In this paper, we present an augmented abstract syntax to model the semantics of interaction with time to completion and recording on time out and relationships between exceptions and their associated activities as guarded activities. We also present a set of transformation rules for construction of timed automata for choreography and scope including exception handler, finalizer blocks and fault and compensation handler.