Abstract
Service Oriented Computing (SOC) is based on service composition, that is, loosely coupled autonomous heterogeneous services, which are collectively composed to implement a particular task. We develop a new calculus for SOC within the framework of CSP process algebra, aiming to improve the verification techniques and to enhance the expressiveness of SOC calculi. This paper presents the part of the calculus that extends CSP with built-in buffers to facilitate direct asynchronous communications. We provide the operational semantics of the calculus and extend the FDR (a CSP model checker) by implementing functions for asynchronous communications.