Data-Aware Design and Verification of Service Compositions 
  with Reo and mCRL2
N. Kokash, C. Krause and E.P. de Vink

Service-based systems can be modeled as stand-alone services coordinated by
external connectors. Reo is a channel-based coordination language with
well-defined semantics that enables a compositional construction of complex
connectors from a set of primitive channels. It has been successfully applied
in the area of web service composition specification as well as in business
process modeling. 
In this paper, we present a mapping from Reo to mCRL2, a specification
language based on the process algebra ACP, extended with data and time. The
mapping enables verification of Reo process models and service compositions
using the mCRL2 model checking facilities. The supporting Eclipse Coordination
Tools suite provides a user-friendly environment for the modeling and
verification process.