Data-Aware Design and Verification of Service Compositions with Reo and mCRL2
Presented at the ACM Symposium on Applied Computing
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.
|ACM||Design Tools and Techniques (acm D.2.2), Specifying and Verifying and Reasoning about Programs (acm F.3.1)|
|THEME||Software (theme 1)|
|Project||Compliance-driven Models, Languages and Architectures for Services|
|Conference||ACM Symposium on Applied Computing|
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.