Data-aware design and verification of service compositions with Reo and mCRL2

N. Kokash; C. Krause; E.P. Vink, de

Data-aware design and verification of service compositions with Reo and mCRL2

N. Kokash, C. Krause, E.P. Vink, de

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

25 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Proceedings 25th ACM Symposium on Applied Computing (SAC'10, Sierre, Switzerland, March 22-26, 2010)
Place of Publication	New York NY
Publisher	Association for Computing Machinery, Inc
Pages	2406-2413
ISBN (Print)	978-1-60558-639-7
Publication status	Published - 2010

Cite this

@inproceedings{46a7ffde26bc48f4aa37c1b770989bf2,

title = "Data-aware design and verification of service compositions with Reo and mCRL2",

abstract = "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.",

author = "N. Kokash and C. Krause and {Vink, de}, E.P.",

year = "2010",

language = "English",

isbn = "978-1-60558-639-7",

pages = "2406--2413",

booktitle = "Proceedings 25th ACM Symposium on Applied Computing (SAC'10, Sierre, Switzerland, March 22-26, 2010)",

publisher = "Association for Computing Machinery, Inc",

address = "United States",

}

Data-aware design and verification of service compositions with Reo and mCRL2. / Kokash, N.; Krause, C.; Vink, de, E.P.
Proceedings 25th ACM Symposium on Applied Computing (SAC'10, Sierre, Switzerland, March 22-26, 2010). New York NY: Association for Computing Machinery, Inc, 2010. p. 2406-2413.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Data-aware design and verification of service compositions with Reo and mCRL2

AU - Kokash, N.

AU - Krause, C.

AU - Vink, de, E.P.

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

UR - http://doi.acm.org/10.1145/1774088.1774590

M3 - Conference contribution

SN - 978-1-60558-639-7

SP - 2406

EP - 2413

BT - Proceedings 25th ACM Symposium on Applied Computing (SAC'10, Sierre, Switzerland, March 22-26, 2010)

PB - Association for Computing Machinery, Inc

CY - New York NY

ER -

Data-aware design and verification of service compositions with Reo and mCRL2

Abstract

Other files and links

Fingerprint

Cite this