Service-based systems can be modeled as stand-alone services coordinated by external connectors. Reo is a channelbased 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.
Additional Metadata
ACM Design Tools and Techniques (acm D.2.2), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
THEME Software (theme 1)
Publisher ACM Press
Project Compliance-driven Models, Languages and Architectures for Services
Conference ACM Symposium on Applied Computing
Citation
Kokash, N, C. (born Köhler, , C.) Krause, ,, & de Vink, E.P. (2010). Data-Aware Design and Verification of Service Compositions with Reo and mCRL2. ACM Press.