Reo + mCRL2 : a framework for model-checking dataflow in service compositions

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

Research output: Contribution to journalArticleAcademicpeer-review

37 Citations (Scopus)
2 Downloads (Pure)

Abstract

The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints imposed by connectors. To ensure that the composed system behaves as intended, we need a wide range of automated verification tools to assist service composition designers. In this paper, we present our framework for the verification of Reo using the mCRL2 toolset. We unify our previous work on mapping various semantic models for Reo, namely, constraint automata, timed constraint automata, coloring semantics and the newly developed action constraint automata, to the process algebraic specification language of mCRL2, address the correctness of this mapping, discuss tool support, and present a detailed example that illustrates the use of Reo empowered with mCRL2 for the analysis of dataflow in service-based process models.
Original languageEnglish
Pages (from-to)187-216
JournalFormal Aspects of Computing
Volume24
Issue number2
DOIs
Publication statusPublished - 2012

Fingerprint

Service Composition
Model checking
Data Flow
Model Checking
Semantics
Connector
Chemical analysis
Automata
Specification languages
Paradigm
Coloring
Algebraic Specification
Service-oriented Computing
Timed Automata
Software engineering
Specification Languages
Synchronization
Tool Support
Modeling Language
Software Engineering

Cite this

@article{8b15d12953bc4cb8b4989a89c62aa8be,
title = "Reo + mCRL2 : a framework for model-checking dataflow in service compositions",
abstract = "The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints imposed by connectors. To ensure that the composed system behaves as intended, we need a wide range of automated verification tools to assist service composition designers. In this paper, we present our framework for the verification of Reo using the mCRL2 toolset. We unify our previous work on mapping various semantic models for Reo, namely, constraint automata, timed constraint automata, coloring semantics and the newly developed action constraint automata, to the process algebraic specification language of mCRL2, address the correctness of this mapping, discuss tool support, and present a detailed example that illustrates the use of Reo empowered with mCRL2 for the analysis of dataflow in service-based process models.",
author = "N. Kokash and C. Krause and {Vink, de}, E.P.",
year = "2012",
doi = "10.1007/s00165-011-0191-6",
language = "English",
volume = "24",
pages = "187--216",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
publisher = "Springer",
number = "2",

}

Reo + mCRL2 : a framework for model-checking dataflow in service compositions. / Kokash, N.; Krause, C.; Vink, de, E.P.

In: Formal Aspects of Computing, Vol. 24, No. 2, 2012, p. 187-216.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Reo + mCRL2 : a framework for model-checking dataflow in service compositions

AU - Kokash, N.

AU - Krause, C.

AU - Vink, de, E.P.

PY - 2012

Y1 - 2012

N2 - The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints imposed by connectors. To ensure that the composed system behaves as intended, we need a wide range of automated verification tools to assist service composition designers. In this paper, we present our framework for the verification of Reo using the mCRL2 toolset. We unify our previous work on mapping various semantic models for Reo, namely, constraint automata, timed constraint automata, coloring semantics and the newly developed action constraint automata, to the process algebraic specification language of mCRL2, address the correctness of this mapping, discuss tool support, and present a detailed example that illustrates the use of Reo empowered with mCRL2 for the analysis of dataflow in service-based process models.

AB - The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints imposed by connectors. To ensure that the composed system behaves as intended, we need a wide range of automated verification tools to assist service composition designers. In this paper, we present our framework for the verification of Reo using the mCRL2 toolset. We unify our previous work on mapping various semantic models for Reo, namely, constraint automata, timed constraint automata, coloring semantics and the newly developed action constraint automata, to the process algebraic specification language of mCRL2, address the correctness of this mapping, discuss tool support, and present a detailed example that illustrates the use of Reo empowered with mCRL2 for the analysis of dataflow in service-based process models.

U2 - 10.1007/s00165-011-0191-6

DO - 10.1007/s00165-011-0191-6

M3 - Article

VL - 24

SP - 187

EP - 216

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

IS - 2

ER -