Information Technology Reference
In-Depth Information
Verification of Context-Dependent
Channel-Based Service Models
Natallia Kokash
1
,,
, Christian Krause
1
,
, and Erik P. de Vink
2
1
CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands
Natallia.Kokash@cwi.nl
2
Technische Universiteit Eindhoven, Den Dolech 2, Eindhoven, The Netherlands
Abstract.
The paradigms of service-oriented computing and model-
driven development are becoming of increasing importance in the field
of software engineering. According to these paradigms, new systems are
composed with added value from existing stand-alone services to sup-
port business processes across organizations. Services comprising a sys-
tem but originating from various sources need to be coordinated. The
Reo coordination language is a state-of-the-art tool supported approach
to channel-based coordination. Reo introduces various types of channels
which can be composed to build complex connectors to represent various
behavioral protocols. This makes Reo suitable for the modeling of service-
based business processes. In previous work we presented a framework for
model checking data-aware Reo connectors using the
mCRL2
toolset. In
this paper, we extend this result with a proof of correctness, evaluation
of optimization techniques, and support for context-sensitive analysis.
1
Introduction
Service-oriented computing is a paradigm that is changing the way modern soft-
ware is designed and developed. Services are autonomous, loosely coupled soft-
ware components with publicly available interfaces that can be invoked by a
client or composed by a third party to achieve a more complex goal. An impor-
tant difference of service-oriented architectures compared to other architectural
solutions is that the owner of a service-based system has very limited control
over the services involved, as generally they run remotely by external companies
which may not even know about each other. Conceptually this is similar to the
idea of exogenous coordination which advocates the separation of computation
(in this case, provided by services) and coordination [1].
One way to coordinate external services is to use a network of communica-
tion channels. Reo is an expressive channel-based coordination language with
computer aided support. Reo introduces various types of channels which can be
composed into complex connectors (also called circuits) to implement interaction
Corresponding author.
Supported by IST COMPAS FP7-ICT-2007-1 project, contract number 215175.
Supported by NWO GLANCE project WoMaLaPaDiA and SYANCO.
