Abstract
The Service Oriented Computing (SOC) paradigm is based on service composition, that is, loosely coupled autonomous heterogeneous services, which are collectively composed to implement a particular task. This paper presents a new calculus, called sbCSP, for SOC within the framework of CSP process algebra, showing how services can be defined, invoked, orchestrated and terminated within session hierarchies. We provide operational and denotational trace semantics for the new calculus, and discuss the relationship between the two semantics. We have implemented the extended calculus in FDR (the CSP model checker) and we have used it in a case study to illustrate the expressivity and simplicity of the session model and its reasoning techniques.