CWI Amsterdam (THE NETHERLANDS)
Eindhoven University of Technology (THE NETHERLANDS)
Hasso Plattner Institute, Potsdam (GERMANY)
Verification of service compositions.
ECT (Extensible Coordination Tools)
CADP (Construction and Analysis of Distributed Processes)
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,
a wide range of automated verification tools is needed to assist
service composition designers.
This work proposes a new framework for the verification of Reo using
formal languages and tools from the concurrency domain, namely the
mCRL2 and CADP tool sets. Several semantic models for Reo (constraint
automata, timed constraint automata, coloring semantics, and action
constraint automata) are mapped to the process algebraic specification
language of mCRL2.
The conversion from Reo to mCRL2 was implemented as an extension to the Extensible Coordination Tools (ECT), which is a framework for modeling, verification, and execution of component-based and service-oriented systems. ECT consists of a set of integrated tools for the Eclipse platform, providing functionalities for converting high-level modeling languages (e.g., UML, BPMN, and BPEL) to Reo, for editing and animation of Reo models, generation of automata-based semantical models from Reo, modeling and verification of QoS properties and tight integrations with external model checking tools such as Vereofy or PRISM. The conversion tool takes as input a Reo circuit and generates automatically a corresponding mCRL2 specification. The tool also provides an integration with CADP by generating labeled transition systems, converting them in the BCG format, and invoking the EVALUATOR model checker from ECT. In [Kokash-Krause-deVink-12] it is reported that:
The newly added plug-in, together with other tools from ECT, provides
a user-friendly environment for graphical modeling of
component/service-based systems and business processes. Since Reo has
an intuitive graphical notation, workflow models designed with ECT look
similar to UML activity diagrams. This facilitates the use of the
framework by any workflow designer. As regards future work, an
interesting direction is to extend the framework with performance
analysis using appropriate tools from CADP.
Natallia Kokash, Christian Krause, and Erik de Vink.
"Reo+mCRL2: A Framework for Model-Checking Dataflow in Service
Formal Aspects of Computing 24(2):187-216, March 2012.
Available on-line at: http://homepages.cwi.nl/~kokash/documents/FACJ11.pdf
or from the CADP Web site in PDF or PostScript
Erik de Vink
Department of Mathematics and Computer Science
Technische Universiteit Eindhoven
Den Dolech 2
|This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software