Using π-calculus for Formal Modeling and Verification of WS-CDL Choreographies

Service-Oriented applications are realized by composing and aggregating existing web services. Orchestration and Choreography are two interaction models for building SOA applications and several standards exist to capture and describe such interactions. The Web Service Choreography Description Language (WS-CDL) is a standard for modeling choreographies. In this paper, we propose a calculus (Chor-calculus) for formal modeling of WS-CDL and we use this language for generating WS-CDL programs. This approach enables the static verification of choreographies using existing pi-calculus model-checker tools and sets the ground for enabling the runtime monitoring of choreographies for behavioral correctness. We validate the calculus for its expressiveness by evaluating the language support for representing workflow, and service interaction, patterns. We demonstrate the use of the HAL toolkit to verify the correctness properties of choreographies.